English
If g is strongly measurable with respect to the pullback along f, then there exists a function h: Y → Z such that g = h ∘ f and h is strongly measurable as well.
Русский
Если g сильно измерима относительно вытянутой по f σ-алгебры, то существует функция h: Y → Z такая, что g = h ∘ f и h также сильно измерима.
LaTeX
$$$$ \exists h : Y \to Z,\; \text{StronglyMeasurable } h \wedge g = h \circ f. $$$$
Lean4
/-- 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`). -/
theorem factorsThrough [TopologicalSpace Z] [PseudoMetrizableSpace Z] [T1Space Z]
(hg : StronglyMeasurable[mY.comap f] g) : g.FactorsThrough f :=
by
borelize Z
exact hg.measurable.factorsThrough
