internlm/Lean-Github huggingface dataset:
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
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ Extendable F c r
Tactic:
exists 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
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)
⊢ HasExtension F G 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
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ HasExtension F G c r
Tactic:
exact
  { gh := uniform_harmonic_lim (fun n ↦ (gs n).gh) gG
    b := by
      intro z
      refine (Filter.Tendsto.limUnder_eq ?_).symm
      simp_rw [← (gs _).b]
      exact fF.tendsto_at z }
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 : C(Real.Angle, ℂ)
Fe : F ∈ closure s
⊢ FrechetUrysohnSpace C(Real.Angle, ℂ)
Tactic:
apply @FirstCountableTopology.frechetUrysohnSpace
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 : 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
⊢ ∀ (n : ℕ), HasExtension (f n) (g n) c r
Tactic:
rw [← hg]
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, ℂ)
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
⊢ ∀ (n : ℕ), HasExtension (f n) ((fun n => Classical.choose ⋯) n) 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, ℂ)
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
⊢ ∀ (n : ℕ), HasExtension (f n) ((fun n => Classical.choose ⋯) n) c r
Tactic:
exact fun n ↦ Classical.choose_spec (e _ (fs n))
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 : 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
⊢ UniformCauchySeqOn g atTop (closedBall c r)
Tactic:
rw [Metric.uniformCauchySeqOn_iff]
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, ℂ)
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
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε
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, ℂ)
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
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε
Tactic:
simp_rw [Metric.tendstoUniformly_iff, Filter.eventually_atTop] at fF
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, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε
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, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε
Tactic:
intro t tp
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, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
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, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Tactic:
rcases fF (t / 4) (by linarith) with ⟨N, H⟩
Proof state after:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Theorem: IsClosed.extendable
Proof state before:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Tactic:
exists N
Proof state after:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Theorem: IsClosed.extendable
Proof state before:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Tactic:
intro a aN b bN z zs
Proof state after:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
⊢ dist (g a z) (g b z) < t
Theorem: IsClosed.extendable
Proof state before:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
⊢ dist (g a z) (g b z) < t
Tactic:
have eab := (gs a).sub (gs b)
Proof state after:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
⊢ dist (g a z) (g b z) < t
Theorem: IsClosed.extendable
Proof state before:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
⊢ dist (g a z) (g b z) < t
Tactic:
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
Proof state after:
case 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
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t