Theorems · Theorem · measure theory

Measurable.exists_eq_measurable_comp

∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [Nonempty Z]
  [inst : MeasurableSpace Z] [StandardBorelSpace Z], Measurable g → ∃ h, Measurable h ∧ g = h ∘ f

If a function g is measurable with respect to the pullback along some function f, then there exists some measurable function h : Y → Z such that g = h ∘ f.

Defined in

Mathlib.MeasureTheory.Function.FactorsThrough

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNonemptyMeasurableSpaceStandardBorelSpace