English
For compact, T2, totally disconnected spaces X, Clopens X is countable iff X is second countable.
Русский
Для компактного, T2, полностью дезконнектированного пространства X множество клиopen эквивалентно счетному базису топологии X.
LaTeX
$$$$ \text{Countable}(\mathrm{Clopens}(X)) \;\Leftrightarrow\; \text{SecondCountableTopology}(X) $$$$
Lean4
theorem countable_iff_secondCountable [T2Space X] [TotallyDisconnectedSpace X] :
Countable (Clopens X) ↔ SecondCountableTopology X :=
by
refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
· let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩
exact (injective_of_le_imp_le f fun a ↦ a).countable
· apply IsTopologicalBasis.eq_generateFrom
exact loc_compact_Haus_tot_disc_of_zero_dim
· have : ∀ (s : Clopens X), ∃ (t : Finset (countableBasis X)), s.1 = t.toSet.sUnion := fun s ↦
eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _ (isBasis_countableBasis X) s.1 s.2.1.isCompact s.2.2
let f : Clopens X → Finset (countableBasis X) := fun s ↦ (this s).choose
have hf : f.Injective := by
intro s t (h : Exists.choose _ = Exists.choose _)
ext1; change s.carrier = t.carrier
rw [(this s).choose_spec, (this t).choose_spec, h]
exact hf.countable
