Commit 2025-03-24 16:18 b7acff0b

feat: if g is measurable wrt to the pullback by f then g is a measurable function of f (#22743) Prove the Doob-Dynkin lemma: let f : X → Y and g : X → Z be such that g is strongly measurable with respect to the pullback by f. Then if Z is nonempty and completely metrizable there exists a measurable function h : Y → Z such that g = h ∘ f.