Theorems · Theorem · general topology

Measurable.measurable_comp_iff_restrict

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

If f : X → Z is a 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 the restriction of g to the range of f is measurable.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceMeasurableSpaceMeasurableSpaceMeasurableSpace.CountablySeparated