English
In a Polish space, a set is clopenable iff it is Borel-measurable.
Русский
В полиш-пространстве множество является клипобелевым тогда и только тогда, когда борелево измеримо.
LaTeX
$$IsClopenable s ↔ MeasurableSet s$$
Lean4
/-- In a Polish space, a set is clopenable if and only if it is Borel-measurable. -/
theorem isClopenable_iff_measurableSet [tγ : TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] :
IsClopenable s ↔ MeasurableSet s := by
-- we already know that a measurable set is clopenable. Conversely, assume that `s` is clopenable.
refine ⟨fun hs => ?_, fun hs => hs.isClopenable⟩
borelize γ
obtain ⟨t', t't, t'_polish, _, s_open⟩ :
∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs
rw [← borel_eq_borel_of_le t'_polish _ t't]
· exact MeasurableSpace.measurableSet_generateFrom s_open
infer_instance
