English
If there exists R > 0 with μ(thickening(R, s)) finite and s is closed, then μ(thickening(r, s)) tends to μ(s) as r → 0.
Русский
Если существует R > 0 такая, что μ(thickening(R, s)) конечна и s замкнуто, то μ(thickening(r, s)) стремится к μ(s) при r → 0.
LaTeX
$$$\\exists R>0, μ(\\mathrm{thickening}(R,s)) \\neq \\infty \\land \\text{IsClosed}(s) \\Rightarrow \\operatorname{Tendsto}\\left(r \\mapsto μ(\\mathrm{thickening}(r,s))\\right)(\\mathcal{N}_{0})(\\mathcal{N}_{μ(s)}).$$$
Lean4
/-- If a closed set has a thickening with finite measure, then the measure of its
`r`-thickenings converge to its measure as `r > 0` tends to `0`. -/
theorem tendsto_measure_thickening_of_isClosed {μ : Measure α} {s : Set α} (hs : ∃ R > 0, μ (thickening R s) ≠ ∞)
(h's : IsClosed s) : Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s)) :=
by
convert tendsto_measure_thickening hs
exact h's.closure_eq.symm
