α : Type u_2
β : Type u_1
ι : Type ?u.64039
E : Type ?u.64042
F : Type ?u.64045
𝕜 : Type ?u.64048
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤
    edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)
α : Type u_2
β : Type u_1
ι : Type ?u.64039
E : Type ?u.64042
F : Type ?u.64045
𝕜 : Type ?u.64048
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (↑(approxOn f hf s y₀ h₀ m) x) (f x)
dsimp only [approxOn, coe_comp, Function.comp]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.64039
E : Type ?u.64042
F : Type ?u.64045
𝕜 : Type ?u.64048
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤
    edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)
exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)