English
The union of a countable family of clopenable sets is clopenable.
Русский
Сумма счётной последовательности множеств, которые можно сделать открытыми и замкнутыми, также clopenable.
LaTeX
$$$\forall n, \text{IsClopenable}(s_n) \Rightarrow \text{IsClopenable}(\bigcup_{n} s_n)$$$
Lean4
theorem iUnion [t : TopologicalSpace α] [PolishSpace α] {s : ℕ → Set α} (hs : ∀ n, IsClopenable (s n)) :
IsClopenable (⋃ n, s n) := by
choose m mt m_polish _ m_open using hs
obtain ⟨t', t'm, -, t'_polish⟩ : ∃ t' : TopologicalSpace α, (∀ n : ℕ, t' ≤ m n) ∧ t' ≤ t ∧ @PolishSpace α t' :=
exists_polishSpace_forall_le m mt m_polish
have A : IsOpen[t'] (⋃ n, s n) := by
apply isOpen_iUnion
intro n
apply t'm n
exact m_open n
obtain ⟨t'', t''_le, t''_polish, h1, h2⟩ :
∃ t'' : TopologicalSpace α, t'' ≤ t' ∧ @PolishSpace α t'' ∧ IsClosed[t''] (⋃ n, s n) ∧ IsOpen[t''] (⋃ n, s n) :=
@IsOpen.isClopenable α t' t'_polish _ A
exact ⟨t'', t''_le.trans ((t'm 0).trans (mt 0)), t''_polish, h1, h2⟩
