English
In an R1 space γ with a Borel measure μ, μ(closure(K)) = μ(K) for every compact K.
Русский
В пространстве γ с борелевской мерой μ для каждого компактного множества K выполняется μ(cl(K)) = μ(K).
LaTeX
$$$\\text{In an } R1\\text{ space } \\gamma\\text{ with a Borel measure } μ,\\; μ(\\overline{K}) = μ(K)\\text{ for all compact } K.$$$
Lean4
/-- In an R₁ topological space with Borel measure `μ`,
the measure of the closure of a compact set `K` is equal to the measure of `K`.
See also `MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact`
for a version that assumes `μ` to be outer regular
but does not assume the `σ`-algebra to be Borel. -/
theorem measure_closure [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : Measure γ) : μ (closure K) = μ K :=
by
refine le_antisymm ?_ (measure_mono subset_closure)
calc
μ (closure K) ≤ μ (toMeasurable μ K) :=
measure_mono <| hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
_ = μ K := measure_toMeasurable ..
