class PiBase.HasClosedDiscreteSubsetCardContinuum (X : Type u_1) [TopologicalSpace X] : Prop

• ex_subset : ∃ (s : Set X), IsDiscrete s ∧ IsClosed s ∧ Cardinal.mk ↑s = Cardinal.continuum