Theorems · Theorem · measure theory

MeasureTheory.Measure.InnerRegularWRT.map

∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {pa qa : Set α → Prop},
  μ.InnerRegularWRT pa qa →
    ∀ {f : α → β},
      AEMeasurable f μ →
        ∀ {pb qb : Set β → Prop},
          (∀ (U : Set β), qb U → qa (f ⁻¹' U)) →
            (∀ (K : Set α), pa K → pb (f '' K)) →
              (∀ (U : Set β), qb U → MeasurableSet U) → (MeasureTheory.Measure.map f μ).InnerRegularWRT pb qb

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace