𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
⊢ IsOpen (↑f '' s)
𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
⊢ IsOpenMap ↑f
intro s hs
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
⊢ IsOpen (↑f '' s)
𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
⊢ IsOpen (↑f '' s)
rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
⊢ IsOpen (↑f '' s)
refine' isOpen_iff.2 fun y yfs => _
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
rcases mem_image_iff_bex.1 yfs with ⟨x, xs, fxy⟩
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
rcases isOpen_iff.1 hs x xs with ⟨ε, εpos, hε⟩
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
⊢ z ∈ ↑f '' s
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
⊢ ∃ ε, ε > 0 ∧ ball y ε ⊆ ↑f '' s
refine' ⟨ε / C, div_pos εpos Cpos, fun z hz => _⟩
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ z ∈ ↑f '' s
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
⊢ z ∈ ↑f '' s
rcases hC (z - y) with ⟨w, wim, wnorm⟩
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ z ∈ ↑f '' s
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ z ∈ ↑f '' s
have : f (x + w) = z := by rw [f.map_add, wim, fxy, add_sub_cancel'_right]
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ↑f (x + w) ∈ ↑f '' s
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ z ∈ ↑f '' s
rw [← this]
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this✝ : ↑f (x + w) = z
this : x + w ∈ ball x ε
⊢ ↑f (x + w) ∈ ↑f '' s
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ↑f (x + w) ∈ ↑f '' s
have : x + w ∈ ball x ε :=
  calc
    dist (x + w) x = ‖w‖ := by
      rw [dist_eq_norm]
      simp
    _ ≤ C * ‖z - y‖ := wnorm
    _ < C * (ε / C) := by
      apply mul_lt_mul_of_pos_left _ Cpos
      rwa [mem_ball, dist_eq_norm] at hz
    _ = ε := mul_div_cancel' _ (ne_of_gt Cpos)
no goals
case 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this✝ : ↑f (x + w) = z
this : x + w ∈ ball x ε
⊢ ↑f (x + w) ∈ ↑f '' s
exact Set.mem_image_of_mem _ (hε this)
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ ↑f (x + w) = z
rw [f.map_add, wim, fxy, add_sub_cancel'_right]
𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ‖x + w - x‖ = ‖w‖
𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ dist (x + w) x = ‖w‖
rw [dist_eq_norm]
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ‖x + w - x‖ = ‖w‖
simp
𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ‖z - y‖ < ε / C
𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ C * ‖z - y‖ < C * (ε / C)
apply mul_lt_mul_of_pos_left _ Cpos
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
inst✝ : CompleteSpace E
surj : Surjective ↑f
s : Set E
hs : IsOpen s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : y ∈ ↑f '' s
x : E
xs : x ∈ s
fxy : ↑f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : ↑f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : ↑f (x + w) = z
⊢ ‖z - y‖ < ε / C
rwa [mem_ball, dist_eq_norm] at hz