measure_closure_eq_of_isCompact — Mathlib

English

For R1-spaces, the measure of the closure of a compact set equals the measure of the set itself under outer regularity.

Русский

На пространствах R1 мера замыкания компактного множества равна мере самого множества под внешней регулярностью.

LaTeX

$$$[R1Space\ α] \; [OuterRegular μ] \; (hk: IsCompact k) \Rightarrow μ(\overline{k}) = μ(k).$$$

Lean4

/-- See also `IsCompact.measure_closure` for a version
that assumes the `σ`-algebra to be the Borel `σ`-algebra but makes no assumptions on `μ`. -/
theorem measure_closure_eq_of_isCompact [R1Space α] [OuterRegular μ] {k : Set α} (hk : IsCompact k) :
    μ (closure k) = μ k := by
  apply le_antisymm ?_ (measure_mono subset_closure)
  simp only [measure_eq_iInf_isOpen k, le_iInf_iff]
  intro u ku u_open
  exact measure_mono (hk.closure_subset_of_isOpen u_open ku)

Похожие утверждения