Theorems · Theorem · measure theory

MeasureTheory.inducedOuterMeasure_preimage

∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ (f : α ≃ α) (Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s),
        (∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs) →
          ∀ {A : Set α},
            (MeasureTheory.inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (MeasureTheory.inducedOuterMeasure m P0 m0) A

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

1 results in Mathlib

Foundations

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