tendsto_measure_Icc_nhdsWithin_right'

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⟩

Похожие утверждения