English
The image of a measurable set in a standard Borel space under a measurable map is analytic.
Русский
Образ измеримого множества в стандартном борелевом пространстве под измеримой картой аналитичен.
LaTeX
$$$\text{MeasurableSet}(s) \Rightarrow \text{AnalyticSet}(f''s) \text{ for } f\;\text{measurable}.$$$
Lean4
/-- The image of a measurable set in a standard Borel space under a measurable map
is an analytic set. -/
theorem _root_.MeasurableSet.analyticSet_image {X Y : Type*} [MeasurableSpace X] [StandardBorelSpace X]
[TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {f : X → Y} [SecondCountableTopology (range f)]
{s : Set X} (hs : MeasurableSet s) (hf : Measurable f) : AnalyticSet (f '' s) :=
by
letI := upgradeStandardBorel X
rw [eq_borel_upgradeStandardBorel X] at hs
rcases hf.exists_continuous with ⟨τ', hle, hfc, hτ'⟩
letI m' : MeasurableSpace X := @borel _ τ'
haveI b' : BorelSpace X := ⟨rfl⟩
have hle := borel_anti hle
exact (hle _ hs).analyticSet.image_of_continuous hfc
