Theorems · Theorem · measure theory

MeasureTheory.Content.measure_eq_content_of_regular

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : MeasurableSpace G]
  [inst_2 : R1Space G] [inst_3 : BorelSpace G],
  μ.ContentRegular → ∀ (K : TopologicalSpace.Compacts G), μ.measure ↑K = μ K

If μ is a regular content, then the measure induced by μ will agree with μ on compact sets.

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceR1SpaceBorelSpace