English
If f: X → Z is a surjective measurable map from a standard Borel space X to a countably separated measurable space Z, then the image space equivalence holds: the pushforward measurable space equals the target's measurable space.
Русский
Если f: X → Z — сюръективное измеримое отображение от стандартного борелова пространства X к счетно-разделяемому измеримому пространству Z, то эквивалентность пространств сохраняется.
LaTeX
$$$\text{Measurable } f \land \text{Surjective } f \Rightarrow \text{MeasurableSpace.map } f\; \bigl(\text{MeasurableSpace } X\bigr) = \text{MeasurableSpace } Z.$$$
Lean4
/-- If `f : X → Z` is a surjective Borel measurable map from a standard Borel space
to a countably separated measurable space, then the preimage of a set `s`
is measurable if and only if the set is measurable.
One implication is the definition of measurability, the other one heavily relies on `X` being a
standard Borel space. -/
theorem measurableSet_preimage_iff_of_surjective [CountablySeparated Z] {f : X → Z} (hf : Measurable f)
(hsurj : Surjective f) {s : Set Z} : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s :=
by
refine ⟨fun h => ?_, fun h => hf h⟩
rcases exists_opensMeasurableSpace_of_countablySeparated Z with ⟨τ, _, _, _⟩
apply AnalyticSet.measurableSet_of_compl
· rw [← image_preimage_eq s hsurj]
exact h.analyticSet_image hf
· rw [← image_preimage_eq sᶜ hsurj]
exact h.compl.analyticSet_image hf
