English
If a set s is clopenable, then its complement sᶜ is also clopenable.
Русский
Если множество s можно сделать открытым и замкнутым в более тонкой топологии, то его комплемент тоже можно.
LaTeX
$$$\text{IsClopenable}(s) \Rightarrow \text{IsClopenable}(s^c)$$$
Lean4
/-- Given a closed set `s` in a Polish space, one can construct a finer Polish topology for
which `s` is both open and closed. -/
theorem _root_.IsClosed.isClopenable [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsClosed s) :
IsClopenable s := by
/- Both sets `s` and `sᶜ` admit a Polish topology. So does their disjoint union `s ⊕ sᶜ`.
Pulling back this topology by the canonical bijection with `α` gives the desired Polish
topology in which `s` is both open and closed. -/
classical
haveI : PolishSpace s := hs.polishSpace
let t : Set α := sᶜ
haveI : PolishSpace t := hs.isOpen_compl.polishSpace
let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› :=
by
simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff, ← continuous_iff_coinduced_le]
exact ⟨continuous_subtype_val, continuous_subtype_val⟩
refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
· rw [← f.induced_symm]
exact f.symm.polishSpace_induced
· rw [isOpen_coinduced, isOpen_sum_iff]
simp only [preimage_preimage, f]
have inl (x : s) : (Equiv.Set.sumCompl s) (Sum.inl x) = x := Equiv.Set.sumCompl_apply_inl ..
have inr (x : ↑sᶜ) : (Equiv.Set.sumCompl s) (Sum.inr x) = x := Equiv.Set.sumCompl_apply_inr ..
simp_rw [t, inl, inr, Subtype.coe_preimage_self]
simp only [isOpen_univ, true_and]
rw [Subtype.preimage_coe_compl']
simp
