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

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

theorem PiBase.WellDefined.hasCountableExtent : WellDefined HasCountableExtent