F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
⊢ ‖L₁ - L₂‖ ≤ 4 * ε

case H
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖L₁ - L₂‖ ≤ 4 * ε
suffices H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
no goals
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
⊢ ‖L₁ - L₂‖ ≤ 4 * ε
rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_left (half_pos hr)] at H
no goals
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖(r / 2) • (L₁ - L₂)‖ = ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖
simp [smul_sub]
case h₁
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r

case h₂
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r + ε * r
apply add_le_add
no goals
case h₁
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r
apply le_of_mem_a h₂ <;> simp [(half_pos hr).le]
no goals
case h₂
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r
apply le_of_mem_a h₁ <;> simp [(half_pos hr).le]
no goals
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ε * r + ε * r = r / 2 * (4 * ε)
ring