English
For a real b and a finite-compact measure μ, μ(Icc(b-δ, b+δ)) tends to μ({b}) as δ → 0+ from the right.
Русский
Пусть μ — конечная по компактам мера на ℝ. Тогда μ(Icc(b-δ, b+δ)) стремится к μ({b}) при δ → 0+ слева (с правого направления).
LaTeX
$$$\\text{tendsto\_measure\_Icc\_nhdsWithin\_right'}(b)$$$
Lean4
theorem tendsto_measure_Icc_nhdsWithin_right' (b : ℝ) :
Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[>] (0 : ℝ)) (𝓝 (μ { b })) :=
by
rw [Real.singleton_eq_inter_Icc]
apply tendsto_measure_biInter_gt (fun r hr ↦ nullMeasurableSet_Icc)
· intro r s _rpos hrs
exact Icc_subset_Icc (by linarith) (by linarith)
· exact ⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩