Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.factorsThrough

∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z}
  [inst : TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z],
  MeasureTheory.StronglyMeasurable g → Function.FactorsThrough g f

If a function g is strongly measurable with respect to the pullback along some function f, then to prove g x = g y it is enough to prove f x = f y. If Z is not empty there exists h : Y → Z such that g = h ∘ f. If Z is also completely metrizable, the factorization map h can be taken to be measurable (see exists_eq_measurable_comp).

Defined in

Mathlib.MeasureTheory.Function.FactorsThrough

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceT1Space