theorem PiBase.hasCountableSpread_iff_discrete_countable (X : Type u_1) [TopologicalSpace X] : HasCountableSpread X ↔ ∀ ⦃s : Set X⦄, IsDiscrete s → s.Countable

A space has countable spread iff all discrete closed subsets are countable.

theorem PiBase.WellDefined.hasCountableSpread : WellDefined HasCountableSpread