internlm/Lean-Github huggingface dataset:
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 0 ≤ 20
Tactic:
positivity
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 0 ≤ 266
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 0 ≤ 20 ^ 233
Tactic:
positivity
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 0 < 125
Tactic:
positivity
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
le : 266 ≤ 20 ^ (233 / 125)
⊢ 469 / 10000 ≤ 1 / 20 - 1619 / 2000 / 266
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
le : 266 ≤ 20 ^ (233 / 125)
⊢ 0 ≤ 1619 / 2000
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
le : 266 ≤ 20 ^ (233 / 125)
⊢ 0 < 266
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
⊢ s.potential c ↑w = s.potential c ↑z ^ 2 ^ (n + 1)
Tactic:
simp only [←hw, ←f_f'_iter, s.potential_eqn_iter]
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 ≤ 469e-4
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 ≤ (↑(2 ^ (n + 1)))⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 ≤ 0.216
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 < ↑(2 ^ (n + 1))
Tactic:
positivity
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
case neg
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∉ s.basin
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
rw [s.potential_eq_one (not_exists.mp m)]
Proof state after:
case neg
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∉ s.basin
⊢ 0.216 ≤ 1
Theorem: le_potential
Proof state before:
case neg
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∉ s.basin
⊢ 0.216 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: spheres_subset_closedBall
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
⊢ sphere c0 r ×ˢ sphere c1 r ⊆ closedBall (c0, c1) r
Tactic:
rw [←closedBall_prod_same, Set.subset_def]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: spheres_subset_closedBall
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
intro z
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ z ∈ sphere c0 r ×ˢ sphere c1 r → z ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: spheres_subset_closedBall
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ z ∈ sphere c0 r ×ˢ sphere c1 r → z ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
simp only [Set.mem_prod, mem_sphere_iff_norm, Complex.norm_eq_abs, Metric.mem_closedBall, and_imp]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → dist z.1 c0 ≤ r ∧ dist z.2 c1 ≤ r
Theorem: spheres_subset_closedBall
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → dist z.1 c0 ≤ r ∧ dist z.2 c1 ≤ r
Tactic:
rw [Complex.dist_eq, Complex.dist_eq]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r
Theorem: spheres_subset_closedBall
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r
Tactic:
intro a b
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b✝ : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
a : Complex.abs (z.1 - c0) = r
b : Complex.abs (z.2 - c1) = r
⊢ Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r
Theorem: spheres_subset_closedBall
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b✝ : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
a : Complex.abs (z.1 - c0) = r
b : Complex.abs (z.2 - c1) = r
⊢ Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r
Tactic:
exact ⟨le_of_eq a, le_of_eq b⟩
Proof state after:
no goals
Theorem: mem_open_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ z ∈ ball c r → z ∈ closedBall c r
Tactic:
simp only [Metric.mem_ball, Metric.mem_closedBall]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ dist z c < r → dist z c ≤ r
Theorem: mem_open_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ dist z c < r → dist z c ≤ r
Tactic:
exact le_of_lt
Proof state after:
no goals
Theorem: mem_sphere_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ z ∈ sphere c r → z ∈ closedBall c r
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs, Metric.mem_closedBall]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ Complex.abs (z - c) = r → dist z c ≤ r
Theorem: mem_sphere_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ Complex.abs (z - c) = r → dist z c ≤ r
Tactic:
exact le_of_eq
Proof state after:
no goals
Theorem: center_not_in_sphere
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : z ∈ sphere c r
⊢ z - c ≠ 0
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs] at zs
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ z - c ≠ 0
Theorem: center_not_in_sphere
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ z - c ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff, zs]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ r ≠ 0
Theorem: center_not_in_sphere
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c z : ℂ
r : ℝ
rp : r > 0
zs : Complex.abs (z - c) = r
⊢ r ≠ 0
Tactic:
exact rp.ne'
Proof state after:
no goals
Theorem: Separate.fc0
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ ContinuousOn (fun z0 => f (z0, w1)) (closedBall c0 r)
Tactic:
refine ContinuousOn.comp h.fc ?_ ?_
Proof state after:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ ContinuousOn (fun z0 => (z0, w1)) (closedBall c0 r)

case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ Set.MapsTo (fun z0 => (z0, w1)) (closedBall c0 r) s
Theorem: Separate.fc0
Proof state before:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ ContinuousOn (fun z0 => (z0, w1)) (closedBall c0 r)
Tactic:
exact ContinuousOn.prod continuousOn_id continuousOn_const
Proof state after:
no goals
Theorem: Separate.fc0
Proof state before:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ Set.MapsTo (fun z0 => (z0, w1)) (closedBall c0 r) s
Tactic:
intro z0 z0m
Proof state after:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ s
Theorem: Separate.fc0
Proof state before:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ s
Tactic:
apply h.rs
Proof state after:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall (c0, c1) r
Theorem: Separate.fc0
Proof state before:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
Proof state after:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: Separate.fc0
Proof state before:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨z0m, mem_open_closed w1m⟩
Proof state after:
no goals
Theorem: Separate.fc1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
⊢ ContinuousOn (fun z1 => f (w0, z1)) (closedBall c1 r)
Tactic:
refine ContinuousOn.comp h.fc ?_ ?_
Proof state after:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
⊢ ContinuousOn (fun z1 => (w0, z1)) (closedBall c1 r)

case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
⊢ Set.MapsTo (fun z1 => (w0, z1)) (closedBall c1 r) s
Theorem: Separate.fc1
Proof state before:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
⊢ ContinuousOn (fun z1 => (w0, z1)) (closedBall c1 r)
Tactic:
exact ContinuousOn.prod continuousOn_const continuousOn_id
Proof state after:
no goals
Theorem: Separate.fc1
Proof state before:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
⊢ Set.MapsTo (fun z1 => (w0, z1)) (closedBall c1 r) s
Tactic:
intro z1 z1m
Proof state after:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ s
Theorem: Separate.fc1
Proof state before:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ s
Tactic:
apply h.rs
Proof state after:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ closedBall (c0, c1) r
Theorem: Separate.fc1
Proof state before:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
Proof state after:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: Separate.fc1
Proof state before:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨w0m, z1m⟩
Proof state after:
no goals
Theorem: Separate.fd0
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ s
Tactic:
apply h.rs
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall (c0, c1) r
Theorem: Separate.fd0
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall (c0, c1) r
Tactic:
rw [←closedBall_prod_same]
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: Separate.fd0
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨w0m, w1m⟩
Proof state after:
no goals
Theorem: Separate.fd1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ s
Tactic:
apply h.rs
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall (c0, c1) r
Theorem: Separate.fd1
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall (c0, c1) r
Tactic:
rw [←closedBall_prod_same]
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall c0 r ×ˢ closedBall c1 r