English
Let μ be a measure, s a subset with μ(cthickening(R, s)) finite for some R > 0, and s closed. Then μ(cthickening(r, s)) tends to μ(s) as r → 0.
Русский
Пусть μ — мера, s — подмножество такое, что μ(cthickening(R, s)) конечна для какого‑то R > 0, и s замкнуто. Тогда μ(cthickening(r, s)) стремится к μ(s) при r → 0.
LaTeX
$$$\\text{IsClosed}(s) \\Rightarrow \\operatorname{Tendsto}\\left(r \\mapsto μ(\\mathrm{cthickening}(r,s))\\right)(\\mathcal{N}_0)(\\mathcal{N}_{μ(s)}).$$$
Lean4
/-- If a closed set has a closed thickening with finite measure, then the measure of its closed
`r`-thickenings converge to its measure as `r` tends to `0`. -/
theorem tendsto_measure_cthickening_of_isClosed {μ : Measure α} {s : Set α} (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞)
(h's : IsClosed s) : Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
by
convert tendsto_measure_cthickening hs
exact h's.closure_eq.symm
