exists_eq_measurable_comp — Mathlib

English

If g is measurable with respect to the pullback σ-algebra, then there exists h: Y → Z that is measurable and g = h ∘ f.

Русский

Если g измерим относительно вытянутой σ-алгебры, существует измеримая h: Y → Z такая, что g = h ∘ f.

LaTeX

$$$$ \exists h : Y \to Z, \; \text{Measurable } h \wedge g = h \circ f. $$$$

Lean4

/-- 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`. -/
theorem _root_.Measurable.exists_eq_measurable_comp [Nonempty Z] [MeasurableSpace Z] [StandardBorelSpace Z]
    (hg : Measurable[mY.comap f] g) : ∃ h : Y → Z, Measurable h ∧ g = h ∘ f :=
  by
  letI := upgradeStandardBorel Z
  obtain ⟨h, mh, hh⟩ := hg.stronglyMeasurable.exists_eq_measurable_comp
  exact ⟨h, mh.measurable, hh⟩

Похожие утверждения