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

• nhds_countable_weak_basis : ∃ (V : X → ℕ → Set X), (∀ (x : X), Antitone (V x) ∧ ∀ (n : ℕ), x ∈ V x n) ∧ ∀ (O : Set X), IsOpen O ↔ ∀ x ∈ O, ∃ (k : ℕ), V x k ⊆ O