𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
⊢ ∀ (x : E), x ∈ A f L r ε → ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
⊢ IsOpen (A f L r ε)
rw [Metric.isOpen_iff]
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
⊢ ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
⊢ ∀ (x : E), x ∈ A f L r ε → ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
rintro x ⟨r', r'_mem, hr'⟩
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
⊢ ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
⊢ ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between r'_mem.1
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
⊢ ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le r'_mem.2)⟩
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
⊢ ∀ (y : E), y ∈ ball x' s → ∀ (z : E), z ∈ ball x' s → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ ∃ ε_1, ε_1 > 0 ∧ ball x ε_1 ⊆ A f L r ε
refine' ⟨r' - s, by linarith, fun x' hx' => ⟨s, this, _⟩⟩
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
⊢ ∀ (y : E), y ∈ ball x' s → ∀ (z : E), z ∈ ball x' s → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
⊢ ∀ (y : E), y ∈ ball x' s → ∀ (z : E), z ∈ ball x' s → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
have B : ball x' s ⊆ ball x r' := ball_subset (le_of_lt hx')
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
hy : y ∈ ball x' s
z : E
hz : z ∈ ball x' s
⊢ ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
⊢ ∀ (y : E), y ∈ ball x' s → ∀ (z : E), z ∈ ball x' s → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
intro y hy z hz
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
hy : y ∈ ball x' s
z : E
hz : z ∈ ball x' s
⊢ ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
exact hr' y (B hy) z (B hz)
no goals
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : E), y ∈ ball x r' → ∀ (z : E), z ∈ ball x r' → ‖f z - f y - ↑L (z - y)‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ r' - s > 0
linarith