English
If f: X → Z is a Borel measurable map from a standard Borel space to a countably separated space, then for any g: Z → β, the measurability of g ∘ f is equivalent to the measurability of the restriction of g to range(f).
Русский
Если f: X → Z — бореллово измеримо и образ range(f) счетко-разделяем, тогда для любого g: Z → β измеримость композиции g ∘ f эквивалентна измеримости ограниченного до образа g.
LaTeX
$$$\text{Measurable } f \rightarrow (\forall g, \text{Measurable}(g \circ f) \iff \text{Measurable}(\text{restrict}(\operatorname{range} f)\; g)).$$$
Lean4
/-- If `f : X → Z` is a Borel measurable map from a standard Borel space
to a countably separated measurable space,
then for any measurable space `β` and `g : Z → β`, the composition `g ∘ f` is
measurable if and only if the restriction of `g` to the range of `f` is measurable. -/
theorem measurable_comp_iff_restrict {f : X → Z} [CountablySeparated (range f)] (hf : Measurable f) {g : Z → β} :
Measurable (g ∘ f) ↔ Measurable (restrict (range f) g) :=
forall₂_congr fun s _ => measurableSet_preimage_iff_preimage_val hf (s := g ⁻¹' s)
