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

• countable_pi_base : ∃ (s : Set (Set X)), s.Countable ∧ IsPiBase s