English
If there exists R > 0 with μ(thickening(R, s)) finite, then μ(thickening(r, s)) tends to μ(closure(s)) as r → 0.
Русский
Если существует R > 0 такая, что μ(thickening(R, s)) конечна, то μ(thickening(r, s)) стремится к μ(closure(s)) при r → 0.
LaTeX
$$$\\text{Exists } R>0, μ(\\mathrm{thickening}(R,s)) \\neq \\infty \\Rightarrow \\operatorname{Tendsto}\\left(r \\mapsto μ(\\mathrm{thickening}(r,s))\\right)(\\mathcal{N}_0)(\\mathcal{N}_{μ(\\overline{s})}).$$$
Lean4
/-- If a set has a thickening with finite measure, then the measures of its `r`-thickenings
converge to the measure of its closure as `r > 0` tends to `0`. -/
theorem tendsto_measure_thickening {μ : Measure α} {s : Set α} (hs : ∃ R > 0, μ (thickening R s) ≠ ∞) :
Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s))) :=
by
rw [closure_eq_iInter_thickening]
exact
tendsto_measure_biInter_gt (fun r _ => isOpen_thickening.nullMeasurableSet) (fun i j _ ij => thickening_mono ij _)
hs
