Theorems · Theorem · measure theory

Measurable.factorsThrough

∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z}
  [inst : MeasurableSpace Z] [MeasurableSingletonClass Z], Measurable g → Function.FactorsThrough g f

If a function g is 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.

Defined in

Mathlib.MeasureTheory.Function.FactorsThrough

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasurableSingletonClass