internlm/Lean-Github huggingface dataset:
Theorem: Extension.maximum_principle
Proof state before:
case intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝
Tactic:
rw [← b] at wh
Proof state after:
case intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
wh : ‖g z‖ ≤ ‖f t‖
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝
Theorem: Extension.maximum_principle
Proof state before:
case intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
wh : ‖g z‖ ≤ ‖f t‖
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝
Tactic:
exact le_trans wh (fb _)
Proof state after:
no goals
Theorem: Extension.maximum_principle
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ Complex.abs w' = 1
Tactic:
simp only [wf, abs_of_pos rp, AbsoluteValue.map_mul, map_inv₀, Complex.abs_ofReal, ← hw']
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ r⁻¹ * r = 1
Theorem: Extension.maximum_principle
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ r⁻¹ * r = 1
Tactic:
field_simp [rp.ne']
Proof state after:
no goals
Theorem: IsClosed.extendable
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
⊢ ∀ f ∈ closure s, Extendable f c r
Tactic:
intro F Fe
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
⊢ Extendable F c r
Tactic:
have fu : FrechetUrysohnSpace C(Real.Angle, ℂ) := by
  apply @FirstCountableTopology.frechetUrysohnSpace
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r
Tactic:
rw [← seqClosure_eq_closure] at Fe
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ seqClosure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ seqClosure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r
Tactic:
rcases Fe with ⟨f, fs, fF⟩
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : Tendsto f atTop (𝓝 F)
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : Tendsto f atTop (𝓝 F)
⊢ Extendable F c r
Tactic:
simp only [ContinuousMap.tendsto_iff_tendstoLocallyUniformly,
  tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace] at fF
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
⊢ Extendable F c r
Tactic:
generalize hg : (fun n ↦ Classical.choose (e _ (fs n))) = g
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ Extendable F c r
Tactic:
have gs : ∀ n, HasExtension (f n) (g n) c r := by
  rw [← hg]; exact fun n ↦ Classical.choose_spec (e _ (fs n))
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ Extendable F c r
Tactic:
have cauchy : UniformCauchySeqOn g atTop (closedBall c r) := by
  rw [Metric.uniformCauchySeqOn_iff]
  simp_rw [Metric.tendstoUniformly_iff, Filter.eventually_atTop] at fF
  intro t tp; rcases fF (t / 4) (by linarith) with ⟨N, H⟩; exists N
  intro a aN b bN z zs
  have eab := (gs a).sub (gs b)
  have fab : ∀ u : Real.Angle, ‖f a u - f b u‖ ≤ t / 2 := by
    intro u
    have ta := H a aN u
    have tb := H b bN u
    rw [← dist_eq_norm]; rw [dist_comm] at ta
    calc dist (f a u) (f b u)
      _ ≤ dist (f a u) (F u) + dist (F u) (f b u) := dist_triangle _ _ _
      _ ≤ t / 4 + t / 4 := by linarith
      _ = t / 2 := by ring_nf
  have m := Extension.maximum_principle eab fab rp z zs
  simp only [Complex.dist_eq, Pi.sub_apply, Complex.norm_eq_abs] at m ⊢
  exact lt_of_le_of_lt m (by linarith)
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
⊢ Extendable F c r
Tactic:
set G := fun z ↦ limUnder atTop fun n ↦ g n z
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ Extendable F c r
Theorem: IsClosed.extendable
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ Extendable F c r
Tactic:
have gG : TendstoUniformlyOn g G atTop (closedBall c r) := by
  apply UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto cauchy
  intro z zs; exact (cauchy.cauchySeq zs).tendsto_limUnder
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F✝ : Type
inst✝⁸ : NormedAddCommGroup F✝
inst✝⁷ : CompleteSpace F✝
inst✝⁶ : NormedSpace ℝ F✝
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F✝
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ Extendable F c r