class PiBase.CountableSetsDiscrete (X : Type u) [TopologicalSpace X] : Prop

• countable_discrete ⦃s : Set X⦄ : s.Countable → IsDiscrete s