internlm/Lean-Github huggingface dataset:
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
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t
Tactic:
have m := Extension.maximum_principle eab fab rp 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
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : ‖(g a - g b) z‖ ≤ t / 2
⊢ 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
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : ‖(g a - g b) z‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t
Tactic:
simp only [Complex.dist_eq, Pi.sub_apply, Complex.norm_eq_abs] at m ⊢
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
m : Complex.abs (g a z - g b z) ≤ t / 2
⊢ Complex.abs (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
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : Complex.abs (g a z - g b z) ≤ t / 2
⊢ Complex.abs (g a z - g b z) < t
Tactic:
exact lt_of_le_of_lt m (by linarith)
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
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
⊢ t / 4 > 0
Tactic:
linarith
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
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
⊢ ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
intro u
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 : ℕ
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
u : Real.Angle
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
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 : ℕ
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
u : Real.Angle
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
have ta := H a aN u
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 : ℕ
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
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
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 : ℕ
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
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
have tb := H b bN u
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 : ℕ
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
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
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 : ℕ
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
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
rw [← dist_eq_norm]
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 : ℕ
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
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2
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 : ℕ
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
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2
Tactic:
rw [dist_comm] at ta
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 : ℕ
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
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2
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 : ℕ
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
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2
Tactic:
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:
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
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
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) (F u) + dist (F u) ((f b) u) ≤ t / 4 + t / 4
Tactic:
linarith
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
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
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ t / 4 + t / 4 = t / 2
Tactic:
ring_nf
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
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
m : Complex.abs (g a z - g b z) ≤ t / 2
⊢ t / 2 < t
Tactic:
linarith
Proof state after:
no goals