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

• countable_local_pi_base (x : X) : ∃ (s : Set (Set X)), ∅ ∉ s ∧ (∀ a ∈ s, IsOpen a) ∧ s.Countable ∧ ∀ U ∈ nhds x, ∃ t ∈ s, t ⊆ U