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

• ex_dense : ∃ (s : Set X), Dense s ∧ Cardinal.mk ↑s ≤ Cardinal.continuum