Theorems · Theorem · measure theory

MeasureTheory.Content.outerMeasure_preimage

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (f : G ≃ₜ G),
  (∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) →
    ∀ (A : Set G), μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1Space