tendsto_measure_Icc_nhdsWithin_right

English

For μ finite on compacts, the right-sided limit of μ(Icc(b-δ, b+δ)) as δ → 0 from the right equals μ({b}).

Русский

Пусть μ имеет конечную меру на компактных множествах. Тогда предел слева направо μ(Icc(b-δ, b+δ)) при δ→0+ равен μ({b}).

LaTeX

$$$\\text{tendsto\_measure\_Icc\_nhdsWithin\_right}(b)$$$

Lean4

theorem tendsto_measure_Icc_nhdsWithin_right (b : ℝ) :
    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[≥] (0 : ℝ)) (𝓝 (μ { b })) :=
  by
  simp only [← nhdsGT_sup_nhdsWithin_singleton, nhdsWithin_singleton, tendsto_sup,
    tendsto_measure_Icc_nhdsWithin_right' μ b, true_and, tendsto_pure_left]
  intro s hs
  simpa using mem_of_mem_nhds hs

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