Theorems · Theorem · measure theory

MeasureTheory.Content.innerContent_comap

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (f : G ≃ₜ G),
  (∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) →
    ∀ (U : TopologicalSpace.Opens G), μ.innerContent ((TopologicalSpace.Opens.comap ↑f) U) = μ.innerContent U

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace