internlm/Lean-Github huggingface dataset:
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M := by simpa [MapsTo] using hM i
Proof state after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
⊢ dist (F i z) (F i ↑w) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e3 : z ∈ closedBall z δ := mem_closedBall_self hδ.le
Proof state after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e4 : w.1 ∈ closedBall z δ := by simpa using (lt_inf_iff.1 hw).1.le
Proof state after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
rw [dist_eq_norm]
Proof state after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ ‖F i z - F i ↑w‖ < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ ‖F i z - F i ↑w‖ < ε
Tactic:
refine ((convex_closedBall _ _).norm_image_sub_le_of_norm_deriv_le e1 e2 e4 e3).trans_lt ?_
Proof state after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ M * ‖z - ↑w‖ < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ M * ‖z - ↑w‖ < ε
Tactic:
have : ‖z - w.val‖ < ε / M := by
  have := (lt_inf_iff.1 hw).2
  rwa [dist_comm, Subtype.dist_eq, dist_eq_norm] at this
Proof state after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ M * ‖z - ↑w‖ < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ M * ‖z - ↑w‖ < ε
Tactic:
convert mul_lt_mul' le_rfl this (norm_nonneg _) hMp
Proof state after:
case h.e'_4
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ ε = M * (ε / M)
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case h.e'_4
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ ε = M * (ε / M)
Tactic:
field_simp [hMp.lt.ne.symm, mul_comm]
Proof state after:
no goals
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Tactic:
obtain ⟨Q, hQ1, hQ2⟩ := h1.deriv hU h2 (closedBall z δ) ⟨h, isCompact_closedBall _ _⟩
Proof state after:
case intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Tactic:
obtain ⟨M, hM⟩ := hQ1.isBounded.subset_closedBall 0
Proof state after:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Tactic:
refine ⟨M ⊔ 1, by simp, fun i => ?_⟩
Proof state after:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
⊢ MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 (M ⊔ 1))
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
⊢ MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 (M ⊔ 1))
Tactic:
exact ((hQ2 i).mono_right hM).mono_right <| closedBall_subset_closedBall le_sup_left
Proof state after:
no goals
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ M ⊔ 1 > 0
Tactic:
simp
Proof state after:
no goals
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
Tactic:
simpa [MapsTo] using hM i
Proof state after:
no goals
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
⊢ ↑w ∈ closedBall z δ
Tactic:
simpa using (lt_inf_iff.1 hw).1.le
Proof state after:
no goals
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ ‖z - ↑w‖ < ε / M
Tactic:
have := (lt_inf_iff.1 hw).2
Proof state after:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : dist w { val := z, property := hz } < ε / M
⊢ ‖z - ↑w‖ < ε / M
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : dist w { val := z, property := hz } < ε / M
⊢ ‖z - ↑w‖ < ε / M
Tactic:
rwa [dist_comm, Subtype.dist_eq, dist_eq_norm] at this
Proof state after:
no goals
Theorem: uniformlyBoundedOn_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ UniformlyBoundedOn Subtype.val U
Tactic:
exact fun K hK => ⟨Q K, hQ K hK, fun f => f.2.2 K hK⟩
Proof state after:
no goals
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsCompact (𝓑 U Q)
Tactic:
have l1 (K) (hK : K ∈ compacts U) : EquicontinuousOn ((↑) : 𝓑 U Q → 𝓒 U) K :=
  (uniformlyBoundedOn_𝓑 hQ).equicontinuousOn hU (fun f => f.2.1) hK
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
⊢ IsCompact (𝓑 U Q)
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
⊢ IsCompact (𝓑 U Q)
Tactic:
have l2 (K) (hK : K ∈ compacts U) (x) (hx : x ∈ K) : ∃ L, IsCompact L ∧ ∀ i : 𝓑 U Q, i.1 x ∈ L :=
  ⟨Q K, hQ K hK, fun f => f.2.2 K hK hx⟩
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsCompact (𝓑 U Q)
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsCompact (𝓑 U Q)
Tactic:
rw [isCompact_iff_compactSpace]
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ CompactSpace ↑(𝓑 U Q)
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ CompactSpace ↑(𝓑 U Q)
Tactic:
refine ArzelaAscoli.compactSpace_of_closedEmbedding (fun K hK => hK.2) ?_ l1 l2
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ ClosedEmbedding (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ ClosedEmbedding (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)
Tactic:
refine ⟨⟨by tauto, fun f g => Subtype.ext⟩, ?_⟩
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsClosed (range (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val))
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsClosed (range (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val))
Tactic:
simpa [range, UniformOnFun.ofFun] using isClosed_𝓑 hU hQ
Proof state after:
no goals
Theorem: isCompact_𝓑
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ Inducing (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)
Tactic:
tauto
Proof state after:
no goals
Theorem: montel
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
h1 : UniformlyBoundedOn F U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
⊢ TotallyBounded (range F)
Tactic:
choose! Q hQ1 hQ2 using h1
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ TotallyBounded (range F)
Theorem: montel
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ TotallyBounded (range F)
Tactic:
have l1 : range F ⊆ 𝓑 U Q := by rintro f ⟨i, rfl⟩ ; exact ⟨h2 i, fun K hK => hQ2 K hK i⟩
Proof state after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
l1 : range F ⊆ 𝓑 U Q
⊢ TotallyBounded (range F)
Theorem: montel
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
l1 : range F ⊆ 𝓑 U Q
⊢ TotallyBounded (range F)
Tactic:
exact totallyBounded_subset l1 <| (isCompact_𝓑 hU hQ1).totallyBounded
Proof state after:
no goals