English
A Borel-measurable set in a Polish space is analytic.
Русский
Подмножество, измеримое в полиш-пространстве, является аналитическим.
LaTeX
$$$[PolishSpace α][MeasurableSpace α][BorelSpace α] \; \text{MeasurableSet}(s) \Rightarrow AnalyticSet(s).$$$
Lean4
/-- A Borel-measurable set in a Polish space is analytic. -/
theorem _root_.MeasurableSet.analyticSet {α : Type*} [t : TopologicalSpace α] [PolishSpace α] [MeasurableSpace α]
[BorelSpace α] {s : Set α} (hs : MeasurableSet s) : AnalyticSet s := by
/- For a short proof (avoiding measurable induction), one sees `s` as a closed set for a finer
topology `t'`. It is analytic for this topology. As the identity from `t'` to `t` is continuous
and the image of an analytic set is analytic, it follows that `s` is also analytic for `t`. -/
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
∃ t' : TopologicalSpace α, t' ≤ t ∧ @PolishSpace α t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs.isClopenable
have A := @IsClosed.analyticSet α t' t'_polish s s_closed
convert @AnalyticSet.image_of_continuous α t' α t s A id (continuous_id_of_le t't)
simp only [id, image_id']
