case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
⊢ A f L r ε ∈ 𝓝[Ioi x] x
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x : ℝ
hx : x ∈ A f L r ε
⊢ A f L r ε ∈ 𝓝[Ioi x] x
rcases hx with ⟨r', rr', hr'⟩
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
⊢ ∃ u, u ∈ Ioi x ∧ Ioo x u ⊆ A f L r ε
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
⊢ A f L r ε ∈ 𝓝[Ioi x] x
rw [mem_nhdsWithin_Ioi_iff_exists_Ioo_subset]
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
⊢ ∃ u, u ∈ Ioi x ∧ Ioo x u ⊆ A f L r ε
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
⊢ ∃ u, u ∈ Ioi x ∧ Ioo x u ⊆ A f L r ε
obtain ⟨s, s_gt, s_lt⟩ : ∃ s : ℝ, r / 2 < s ∧ s < r' := exists_between rr'.1
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ ∃ u, u ∈ Ioi x ∧ Ioo x u ⊆ A f L r ε
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
⊢ ∃ u, u ∈ Ioi x ∧ Ioo x u ⊆ A f L r ε
have : s ∈ Ioc (r / 2) r := ⟨s_gt, le_of_lt (s_lt.trans_le rr'.2)⟩
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ ∀ (y : ℝ), y ∈ Icc x' (x' + s) → ∀ (z : ℝ), z ∈ Icc x' (x' + s) → ‖f z - f y - (z - y) • L‖ ≤ ε * r
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ ∃ u, u ∈ Ioi x ∧ Ioo x u ⊆ A f L r ε
refine' ⟨x + r' - s, by simp only [mem_Ioi]; linarith, fun x' hx' => ⟨s, this, _⟩⟩
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
⊢ ∀ (y : ℝ), y ∈ Icc x' (x' + s) → ∀ (z : ℝ), z ∈ Icc x' (x' + s) → ‖f z - f y - (z - y) • L‖ ≤ ε * r
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ ∀ (y : ℝ), y ∈ Icc x' (x' + s) → ∀ (z : ℝ), z ∈ Icc x' (x' + s) → ‖f z - f y - (z - y) • L‖ ≤ ε * r
have A : Icc x' (x' + s) ⊆ Icc x (x + r') := by
  apply Icc_subset_Icc hx'.1.le
  linarith [hx'.2]
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
y : ℝ
hy : y ∈ Icc x' (x' + s)
z : ℝ
hz : z ∈ Icc x' (x' + s)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
⊢ ∀ (y : ℝ), y ∈ Icc x' (x' + s) → ∀ (z : ℝ), z ∈ Icc x' (x' + s) → ‖f z - f y - (z - y) • L‖ ≤ ε * r
intro y hy z hz
no goals
case intro.intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
y : ℝ
hy : y ∈ Icc x' (x' + s)
z : ℝ
hz : z ∈ Icc x' (x' + s)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r
exact hr' y (A hy) z (A hz)
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ x < x + r' - s
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ x + r' - s ∈ Ioi x
simp only [mem_Ioi]
no goals
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
⊢ x < x + r' - s
linarith
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ x' + s ≤ x + r'
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ Icc x' (x' + s) ⊆ Icc x (x + r')
apply Icc_subset_Icc hx'.1.le
no goals
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
L : F
r ε x r' : ℝ
rr' : 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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ x' + s ≤ x + r'
linarith [hx'.2]