Theorems · Theorem · measure theory

MeasureTheory.Measure.QuasiMeasurePreserving.measurable

∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.Measure.QuasiMeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.Measure.QuasiMeasurePreserving._auto_3},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → Measurable f

Defined in

Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Cited by

12 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms