α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : edist y₀ (↑(approxOn f hf s y₀ h₀ n) x) ≤ edist y₀ (f x) + edist y₀ (f x)
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
have := edist_approxOn_y0_le hf h₀ x n
α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : ↑‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖₊ ≤ ↑‖f x - y₀‖₊ + ↑‖f x - y₀‖₊
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : edist y₀ (↑(approxOn f hf s y₀ h₀ n) x) ≤ edist y₀ (f x) + edist y₀ (f x)
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
repeat' rw [edist_comm y₀, edist_eq_coe_nnnorm_sub] at this
no goals
α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : ↑‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖₊ ≤ ↑‖f x - y₀‖₊ + ↑‖f x - y₀‖₊
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
exact_mod_cast this
α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : ↑‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖₊ ≤ ↑‖f x - y₀‖₊ + ↑‖f x - y₀‖₊
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
α : Type ?u.11745
β : Type u_2
ι : Type ?u.11751
E : Type u_1
F : Type ?u.11757
𝕜 : Type ?u.11760
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : ↑‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖₊ ≤ ↑‖f x - y₀‖₊ + ↑‖f x - y₀‖₊
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
rw [edist_comm y₀, edist_eq_coe_nnnorm_sub] at this