English
If f: X → Z is a measurable map with countably separated range, and the range of f is measurable, then measurability of the preimage of s is equivalent to measurability of s ∩ range f.
Русский
Если f: X → Z измеримо и range(f) счетно разделимо и измеримо, то MeasurableSet(f^{-1}(s)) эквивалентно MeasurableSet(s ∩ range f).
LaTeX
$$$[CountablySeparated (range f)] (hf : Measurable f) (hr : MeasurableSet (range f)) {s} :\;\ \ MeasurableSet(f^{-1}(s)) \iff MeasurableSet(s \cap range f).$$$
Lean4
/-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
countably separated measurable space and the range of `f` is measurable,
then the preimage of a set `s` is measurable
if and only if the intersection with `Set.range f` is measurable. -/
theorem measurableSet_preimage_iff_inter_range {f : X → Z} [CountablySeparated (range f)] (hf : Measurable f)
(hr : MeasurableSet (range f)) {s : Set Z} : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f) := by
rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm, ←
(MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]
