α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 - f x‖₊ ≤ ‖f x - y₀‖₊
have := edist_approxOn_le hf h₀ x n
α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (f x) y₀
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
rw [edist_comm y₀] at this
α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 - f x‖₊ ≤ ↑‖f x - y₀‖₊
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (f x) y₀
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
simp only [edist_nndist, nndist_eq_nnnorm] at this
no goals
α : Type ?u.8872
β : Type u_2
ι : Type ?u.8878
E : Type u_1
F : Type ?u.8884
𝕜 : Type ?u.8887
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 - f x‖₊ ≤ ↑‖f x - y₀‖₊
⊢ ‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
exact_mod_cast this