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 ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : 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
⊢ x ∈ 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 ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ
rintro x ⟨r', r'r, hr'⟩
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 ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : 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
y : E
hy : y ∈ ball x r'
z : E
hz : z ∈ ball x r'
⊢ 0 ≤ 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 ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : 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
⊢ x ∈ A f L r δ
refine' ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans (mul_le_mul_of_nonneg_right h _)⟩
no goals
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 ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : 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
y : E
hy : y ∈ ball x r'
z : E
hz : z ∈ ball x r'
⊢ 0 ≤ r
linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x]