tendsto_measure_Icc — Mathlib

English

Let μ be a finite measure on ℝ with no atoms. For every real number b, the mass μ([b−δ, b+δ]) tends to 0 as δ → 0.

Русский

Пусть μ — конечная мера на ℝ без атомов. Для каждого числа b мера множества [b−δ, b+δ] стремится к 0 при δ → 0.

LaTeX

$$$$\\forall b \\in \\mathbb{R}, \\lim_{\\delta \\to 0} \\mu([b-\\delta, b+\\delta]) = 0.$$$$

Lean4

theorem tendsto_measure_Icc [NoAtoms μ] (b : ℝ) : Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝 (0 : ℝ)) (𝓝 0) :=
  by
  rw [← nhdsLT_sup_nhdsGE, tendsto_sup]
  constructor
  · apply tendsto_const_nhds.congr'
    filter_upwards [self_mem_nhdsWithin] with r (hr : r < 0)
    rw [Icc_eq_empty (by linarith), measure_empty]
  · simpa only [measure_singleton] using tendsto_measure_Icc_nhdsWithin_right μ b

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