Theorems · Theorem · measure theory

IsCompact.measure_closure

∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ},
  IsCompact K → ∀ (μ : MeasureTheory.Measure γ), μ (closure K) = μ K

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.

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Cited by

10 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceR1Space