Theorems · Theorem · measure theory

MeasurableEmbedding.ae_map_iff

∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ {p : β → Prop} {μ : MeasureTheory.Measure α},
      (∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

6 results in Mathlib

Foundations

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