case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : ℝ), y ∈ Icc x (x + r') → ∀ (z : ℝ), z ∈ Icc x (x + r') → ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x ∈ A f L r δ
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ
rintro x ⟨r', r'r, hr'⟩
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : ℝ), y ∈ Icc x (x + r') → ∀ (z : ℝ), z ∈ Icc x (x + r') → ‖f z - f y - (z - y) • L‖ ≤ ε * r
y : ℝ
hy : y ∈ Icc x (x + r')
z : ℝ
hz : z ∈ Icc x (x + r')
⊢ 0 ≤ r
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : ℝ), y ∈ Icc x (x + r') → ∀ (z : ℝ), z ∈ Icc x (x + r') → ‖f z - f y - (z - y) • L‖ ≤ ε * 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
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ (y : ℝ), y ∈ Icc x (x + r') → ∀ (z : ℝ), z ∈ Icc x (x + r') → ‖f z - f y - (z - y) • L‖ ≤ ε * r
y : ℝ
hy : y ∈ Icc x (x + r')
z : ℝ
hz : z ∈ Icc x (x + r')
⊢ 0 ≤ r
linarith [hy.1, hy.2, r'r.2]