English
Let α be a proper metric space and μ a finite measure on compacts; for a compact set s, the measure of its r-thickening tends to μ(s) as r → 0.
Русский
Пусть α — нормированное метрическое пространство, μ — сколь угодно ограниченная мера на компактах; для компактного множества s мера его r‑толщения стремится к μ(s) при r → 0.
LaTeX
$$$\\text{Tendsto}(\\lambda r. μ(\\mathrm{cthickening}(r, s)))\\,(\\mathcal{N}0)\\,(\\mathcal{N}(μ s))$$$
Lean4
/-- Given a compact set in a proper space, the measure of its `r`-closed thickenings converges to
its measure as `r` tends to `0`. -/
theorem tendsto_measure_cthickening_of_isCompact [MetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
[ProperSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {s : Set α} (hs : IsCompact s) :
Tendsto (fun r => μ (Metric.cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
tendsto_measure_cthickening_of_isClosed ⟨1, zero_lt_one, hs.isBounded.cthickening.measure_lt_top.ne⟩ hs.isClosed
