𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have A : (⋃ n : ℕ, closure (f '' ball 0 n)) = Set.univ := by
  refine' Subset.antisymm (subset_univ _) fun y _ => _
  rcases surj y with ⟨x, hx⟩
  rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
  refine' mem_iUnion.2 ⟨n, subset_closure _⟩
  refine' (mem_image _ _ _).2 ⟨x, ⟨_, hx⟩⟩
  rwa [mem_ball, dist_eq_norm, sub_zero]
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
this : ∃ n x, x ∈ interior (closure (↑f '' ball 0 ↑n))
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
have : ∃ (n : ℕ)(x : _), x ∈ interior (closure (f '' ball 0 n)) :=
  nonempty_interior_of_iUnion_of_closed (fun n => isClosed_closure) A
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
this : ∃ n x ε, ε > 0 ∧ ball x ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
this : ∃ n x, x ∈ interior (closure (↑f '' ball 0 ↑n))
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
simp only [mem_interior_iff_mem_nhds, Metric.mem_nhds_iff] at this
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
this : ∃ n x ε, ε > 0 ∧ ball x ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩
case intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
case intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n ≥ 0

case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
refine' ⟨(ε / 2)⁻¹ * ‖c‖ * 2 * n, _, fun y => _⟩
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
⊢ (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
refine' Subset.antisymm (subset_univ _) fun y _ => _
case intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
rcases surj y with ⟨x, hx⟩
case intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
case intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
case intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ y ∈ ↑f '' ball 0 ↑n
case intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ y ∈ ⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)
refine' mem_iUnion.2 ⟨n, subset_closure _⟩
case intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ x ∈ ball 0 ↑n
case intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ y ∈ ↑f '' ball 0 ↑n
refine' (mem_image _ _ _).2 ⟨x, ⟨_, hx⟩⟩
no goals
case intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
y : F
x✝ : y ∈ Set.univ
x : E
hx : ↑f x = y
n : ℕ
hn : ‖x‖ < ↑n
⊢ x ∈ ball 0 ↑n
rwa [mem_ball, dist_eq_norm, sub_zero]
case intro.intro.intro.intro.intro.refine'_1.refine'_1
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ (ε / 2)⁻¹

case intro.intro.intro.intro.intro.refine'_1.refine'_2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ ↑n
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n ≥ 0
refine' mul_nonneg (mul_nonneg (mul_nonneg _ (norm_nonneg _)) (by norm_num)) _
no goals
case intro.intro.intro.intro.intro.refine'_1.refine'_1
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ (ε / 2)⁻¹

case intro.intro.intro.intro.intro.refine'_1.refine'_2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ ↑n
exacts [inv_nonneg.2 (div_nonneg (le_of_lt εpos) (by norm_num)), n.cast_nonneg]
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ 2
norm_num
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 ≤ 2
norm_num
case pos
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y = 0
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

case neg
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
by_cases hy : y = 0
case pos
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y = 0
⊢ dist (↑f 0) y ≤ 1 / 2 * ‖y‖ ∧ ‖0‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case pos
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y = 0
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
use 0
no goals
case pos
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y = 0
⊢ dist (↑f 0) y ≤ 1 / 2 * ‖y‖ ∧ ‖0‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
simp [hy]
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rcases rescale_to_shell hc (half_pos εpos) hy with ⟨d, hd, ydlt, -, dinv⟩
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
let δ := ‖d‖ * ‖y‖ / 4
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
have δpos : 0 < δ := div_pos (mul_pos (norm_pos_iff.2 hd) (norm_pos_iff.2 hy)) (by norm_num)
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
have : a + d • y ∈ ball a ε := by
  simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)]
case neg.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₁, z₁im, h₁⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
x₁ : E
hx₁ : x₁ ∈ ball 0 ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rcases(mem_image _ _ _).1 z₁im with ⟨x₁, hx₁, xz₁⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : x₁ ∈ ball 0 ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
x₁ : E
hx₁ : x₁ ∈ ball 0 ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rw [← xz₁] at h₁
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : x₁ ∈ ball 0 ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rw [mem_ball, dist_eq_norm, sub_zero] at hx₁
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
have : a ∈ ball a ε := by
  simp
  exact εpos
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₂ : dist a z₂ < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₂, z₂im, h₂⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₂ : dist a z₂ < δ
x₂ : E
hx₂ : x₂ ∈ ball 0 ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₂ : dist a z₂ < δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rcases(mem_image _ _ _).1 z₂im with ⟨x₂, hx₂, xz₂⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : x₂ ∈ ball 0 ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
h₂ : dist a z₂ < δ
x₂ : E
hx₂ : x₂ ∈ ball 0 ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rw [← xz₂] at h₂
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : x₂ ∈ ball 0 ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rw [mem_ball, dist_eq_norm, sub_zero] at hx₂
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
let x := x₁ - x₂
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : ‖↑f (d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
have J : ‖f (d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖ :=
  calc
    ‖f (d⁻¹ • x) - y‖ = ‖d⁻¹ • f x - (d⁻¹ * d) • y‖ := by
      rwa [f.map_smul _, inv_mul_cancel, one_smul]
    _ = ‖d⁻¹ • (f x - d • y)‖ := by rw [mul_smul, smul_sub]
    _ = ‖d‖⁻¹ * ‖f x - d • y‖ := by rw [norm_smul, norm_inv]
    _ ≤ ‖d‖⁻¹ * (2 * δ) := by
      apply mul_le_mul_of_nonneg_left I
      rw [inv_nonneg]
      exact norm_nonneg _
    _ = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2 := by
      simp only
      ring
    _ = ‖y‖ / 2 := by
      rw [inv_mul_cancel, one_mul]
      simp [norm_eq_zero, hd]
    _ = 1 / 2 * ‖y‖ := by ring
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : ‖↑f (d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
rw [← dist_eq_norm] at J
no goals
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
K : ‖d⁻¹ • x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
⊢ ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
exact ⟨d⁻¹ • x, J, K⟩
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
⊢ 0 < 4
norm_num
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
⊢ a + d • y ∈ ball a ε
simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)]
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ 0 < ε
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ a ∈ ball a ε
simp
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
⊢ 0 < ε
exact εpos
case e_a
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x - d • y‖ = ‖↑f x₁ - (a + d • y) - (↑f x₂ - a)‖
congr 1
case e_a
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x₁ - ↑f x₂ - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
case e_a
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
simp only [f.map_sub]
no goals
case e_a
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ↑f x₁ - ↑f x₂ - d • y = ↑f x₁ - (a + d • y) - (↑f x₂ - a)
abel
case h₁
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₁ - (a + d • y)‖ ≤ δ

case h₂
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₂ - a‖ ≤ δ
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₁ - (a + d • y)‖ + ‖↑f x₂ - a‖ ≤ δ + δ
apply add_le_add
case h₁
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ dist (a + d • y) (↑f x₁) ≤ δ
case h₁
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₁ - (a + d • y)‖ ≤ δ
rw [← dist_eq_norm, dist_comm]
no goals
case h₁
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ dist (a + d • y) (↑f x₁) ≤ δ
exact le_of_lt h₁
case h₂
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ dist a (↑f x₂) ≤ δ
case h₂
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖↑f x₂ - a‖ ≤ δ
rw [← dist_eq_norm, dist_comm]
no goals
case h₂
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
⊢ dist a (↑f x₂) ≤ δ
exact le_of_lt h₂
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖↑f (d⁻¹ • x) - y‖ = ‖d⁻¹ • ↑f x - (d⁻¹ * d) • y‖
rwa [f.map_smul _, inv_mul_cancel, one_smul]
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d⁻¹ • ↑f x - (d⁻¹ * d) • y‖ = ‖d⁻¹ • (↑f x - d • y)‖
rw [mul_smul, smul_sub]
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d⁻¹ • (↑f x - d • y)‖ = ‖d‖⁻¹ * ‖↑f x - d • y‖
rw [norm_smul, norm_inv]
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ 0 ≤ ‖d‖⁻¹
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * ‖↑f x - d • y‖ ≤ ‖d‖⁻¹ * (2 * δ)
apply mul_le_mul_of_nonneg_left I
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ 0 ≤ ‖d‖
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ 0 ≤ ‖d‖⁻¹
rw [inv_nonneg]
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ 0 ≤ ‖d‖
exact norm_nonneg _
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * (2 * (‖d‖ * ‖y‖ / 4)) = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * (2 * δ) = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2
simp only
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * (2 * (‖d‖ * ‖y‖ / 4)) = ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2
ring
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖ ≠ 0
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖⁻¹ * ‖d‖ * ‖y‖ / 2 = ‖y‖ / 2
rw [inv_mul_cancel, one_mul]
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖d‖ ≠ 0
simp [norm_eq_zero, hd]
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
⊢ ‖y‖ / 2 = 1 / 2 * ‖y‖
ring
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖d⁻¹ • x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖
rw [norm_smul, norm_inv]
case refine'_1
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖x₁ - x₂‖ ≤ ↑n + ↑n

case refine'_2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ 0 ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖d‖⁻¹ * ‖x₁ - x₂‖ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (↑n + ↑n)
refine' mul_le_mul dinv _ (norm_nonneg _) _
no goals
case refine'_1
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖x₁ - x₂‖ ≤ ↑n + ↑n
exact le_trans (norm_sub_le _ _) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂))
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ 0 ≤ (ε / 2)⁻¹
case refine'_2
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ 0 ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
apply mul_nonneg (mul_nonneg _ (norm_nonneg _)) (norm_nonneg _)
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ 0 ≤ (ε / 2)⁻¹
exact inv_nonneg.2 (le_of_lt (half_pos εpos))
no goals
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝ : CompleteSpace F
surj : Surjective ↑f
A : (⋃ (n : ℕ), closure (↑f '' ball 0 ↑n)) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure ((fun a => ↑f a) '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : ¬y = 0
d : 𝕜
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (↑f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : ↑f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ (fun a => ↑f a) '' ball 0 ↑n
x₂ : E
h₂ : dist a (↑f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : ↑f x₂ = z₂
x : E := x₁ - x₂
I : ‖↑f x - d • y‖ ≤ 2 * δ
J : dist (↑f (d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (↑n + ↑n) = (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
ring