measurableSet_of_compl — Mathlib

English

In a Hausdorff space, an analytic set with an analytic complement is measurable.

Русский

В гаммах пространстве Хаусдорфа аналитическое множество с аналитическим дополнением измеримо.

LaTeX

$$$\text{AnalyticSet}(s) \land \text{AnalyticSet}(s^c) \Rightarrow \text{MeasurableSet}(s).$$$

Lean4

/-- **Suslin's Theorem**: in a Hausdorff topological space, an analytic set with an analytic
complement is measurable. -/
theorem measurableSet_of_compl [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (hs : AnalyticSet s)
    (hsc : AnalyticSet sᶜ) : MeasurableSet s :=
  by
  rcases hs.measurablySeparable hsc disjoint_compl_right with ⟨u, hsu, hdu, hmu⟩
  obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)
  exact hmu

Похожие утверждения