English
If a function g is measurable with respect to the pullback σ-algebra along f, then g factors through f; i.e., there exists h such that g = h ∘ f.
Русский
Если функция g измерима относительно вытянутой по f σ-алгебры, то g факторизуется через f; то есть существует h: Y → Z с g = h ∘ f.
LaTeX
$$$$ \exists h : Y \to Z,\; g = h \circ f. $$$$
Lean4
/-- 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`. -/
theorem _root_.Measurable.factorsThrough [MeasurableSpace Z] [MeasurableSingletonClass Z]
(hg : Measurable[mY.comap f] g) : g.FactorsThrough f :=
by
refine fun x₁ x₂ h ↦ eq_of_mem_singleton ?_
obtain ⟨s, -, hs⟩ := hg (measurableSet_singleton (g x₂))
rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
