Theorems · Theorem · general topology

Measurable.measurable_comp_iff_of_surjective

∀ {X : Type u_3} {Z : Type u_5} {β : Type u_6} [inst : MeasurableSpace X] [StandardBorelSpace X]
  [inst_2 : MeasurableSpace β] [inst_3 : MeasurableSpace Z] [MeasurableSpace.CountablySeparated Z] {f : X → Z},
  Measurable f → Function.Surjective f → ∀ {g : Z → β}, Measurable (g ∘ f) ↔ Measurable g

If f : X → Z is a surjective Borel measurable map from a standard Borel space to a countably separated measurable space, then for any measurable space α and g : Z → α, the composition g ∘ f is measurable if and only if g is measurable.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceMeasurableSpaceMeasurableSpaceMeasurableSpace.CountablySeparated