theorem PiBase.Set.countable_of_setminus_singleton {α : Type u_1} {s : Set α} {a : α} (h : (s \ {a}).Countable) : s.Countable

theorem PiBase.countableChainCondition_iff_ex_nonempty_chain (X : Type u_1) [TopologicalSpace X] : CountableChainCondition X ↔ ∀ ⦃S : Set (Set X)⦄, S.PairwiseDisjoint id → (∀ s ∈ S, IsOpen s) → ∅ ∉ S → S.Countable

theorem PiBase.WellDefined.countableChainCondition : WellDefined CountableChainCondition