English
Given a measurable set in a Polish space, there exists a finer Polish topology in which the set is both open and closed (clopen).
Русский
Для измеримого множества в полиш-пространстве существует более тонкая полиш-структура, в которой множество открыто и закрыто.
LaTeX
$$$\exists t' \le t: \ IsPolishSpace t' \land IsOpen_{t'}(s) \land IsClosed_{t'}(s).$$$
Lean4
/-- Given a Borel-measurable set in a Polish space, there exists a finer Polish topology making
it clopen. This is in fact an equivalence, see `isClopenable_iff_measurableSet`. -/
theorem _root_.MeasurableSet.isClopenable [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {s : Set α}
(hs : MeasurableSet s) : IsClopenable s := by
revert s
apply MeasurableSet.induction_on_open
· exact fun u hu => hu.isClopenable
· exact fun u _ h'u => h'u.compl
· exact fun f _ _ hf => IsClopenable.iUnion hf
