1. FormalConjectures
  2. Paper
  3. WeaklyFirstCountable
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Conjectures about Weakly First Countable spaces

This file formalizes the notion of a weakly first countable topological space and some conjectures around those.

References:

    [Ar2013] Arhangeliski, Alexandr. "Selected old open problems in general topology." Buletinul Academiei de Ştiinţe a Republicii Moldova. Matematica 73.2-3 (2013): 37-46. https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46).pdf.pdf

    [Ya1976] Yakovlev, N. N. "On the theory of o-metrizable spaces." Doklady Akademii Nauk. Vol. 229. No. 6. Russian Academy of Sciences, 1976. https://www.mathnet.ru/links/016f74007f9f96fa3aadae05cbd98457/dan40570.pdf (in Russian)

open TopologicalSpace Topology Filteropen scoped Cardinalnamespace WeaklyFirstCountableuniverse u

A topological space $X$ is called weakly first countable if there exists a function $N : X → ℕ → Set X$, such that:

    For all $x : X, n : ℕ$ we have $x ∈ V x n$

    For all $x : X, n : ℕ$: $V x (n + 1) ⊆ V x n$

    $O ⊆ X$ is open iff $∀ x ∈ O, ∃ n : ℕ, V x n ⊆ O$

class WeaklyFirstCountableTopology (X : Type*) [TopologicalSpace X] : Prop where 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

A cellular family is a pairwise-disjoint collection of nonempty open sets.

def IsCellularFamily (X : Type u) [TopologicalSpace X] (F : Set (Set X)) : Prop := F.PairwiseDisjoint id ∧ ∀ U ∈ F, IsOpen U ∧ U.Nonempty

The Souslin number of a topological space is the supremum of the cardinalities of its cellular families.

noncomputable def souslinNumber (X : Type u) [TopologicalSpace X] : Cardinal.{u} := ⨆ F : {F : Set (Set X) // IsCellularFamily X F}, #(F : Set (Set X))

A space has countable Souslin number when its Souslin number is at most ℵ₀.

class HasCountableSouslinNumber (X : Type u) [TopologicalSpace X] : Prop where souslinNumber_le : souslinNumber X ≤ ℵ₀

There are weakly first countable spaces which are not first countable, for example the Arens Space.

@[category textbook, AMS 54] theorem exists_weakly_first_countable_not_first_countable : ∃ (X : Type) (_ : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ ¬ FirstCountableTopology X := ⊢ ∃ X x, WeaklyFirstCountableTopology X ∧ ¬FirstCountableTopology X All goals completed! 🐙

Every first countable space is weakly first countable, simply take $N x$ as a countable neighborhood basis of $x$.

X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set X⊢ (∀ x ∈ O, O ∈ 𝓝 x) ↔ ∀ x ∈ O, ∃ k, U x k ⊆ O X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set X⊢ (∀ x ∈ O, O ∈ 𝓝 x) → ∀ x ∈ O, ∃ k, U x k ⊆ OX:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set X⊢ (∀ x ∈ O, ∃ k, U x k ⊆ O) → ∀ x ∈ O, O ∈ 𝓝 x X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set X⊢ (∀ x ∈ O, O ∈ 𝓝 x) → ∀ x ∈ O, ∃ k, U x k ⊆ OX:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set X⊢ (∀ x ∈ O, ∃ k, U x k ⊆ O) → ∀ x ∈ O, O ∈ 𝓝 x X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set Xh:∀ x ∈ O, ∃ k, U x k ⊆ Ox:Xhx:x ∈ O⊢ O ∈ 𝓝 x X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set Xh:∀ x ∈ O, O ∈ 𝓝 xx:Xhx:x ∈ O⊢ ∃ k, U x k ⊆ O All goals completed! 🐙 X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set Xh:∀ x ∈ O, ∃ k, U x k ⊆ Ox:Xhx:x ∈ O⊢ O ∈ 𝓝 x X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis xU:X → ℕ → Set X := fun x ↦ ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x)O:Set Xh:∀ x ∈ O, ∃ k, U x k ⊆ Ox:Xhx:x ∈ On:ℕhn:U x n ⊆ O⊢ O ∈ 𝓝 x All goals completed! 🐙

Every separable space has countable Souslin number.

@[category test, AMS 54] instance hasCountableSouslinNumber_of_separable (X : Type u) [TopologicalSpace X] [SeparableSpace X] : HasCountableSouslinNumber X where souslinNumber_le := X:Type uinst✝¹:TopologicalSpace Xinst✝:SeparableSpace X⊢ souslinNumber X ≤ ℵ₀ X:Type uinst✝¹:TopologicalSpace Xinst✝:SeparableSpace XF:{ F // IsCellularFamily X F }⊢ #↑↑F ≤ ℵ₀ All goals completed! 🐙

Problem 2 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space X such that $𝔠 < |X|$.

Note: [Ar2013] uses a blanket convention that all spaces are Tychonoff and "compact" means compact Hausdorff.

@[category research open, AMS 54] theorem existsWeaklyFirstCountableCompactBig : answer(sorry) ↔ ∃ (X : Type) (_ : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ 𝔠 < #X := ⊢ True ↔ ∃ X x, WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ 𝔠 < #X All goals completed! 🐙

Problem 3 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space which is not first countable.

Note: [Ar2013] uses a blanket convention that all spaces are Tychonoff and "compact" means compact Hausdorff.

@[category research open, AMS 54] theorem existsWeaklyFirstCountableCompactNotFirstCountable : ∃ (X : Type) (_ : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ ¬ FirstCountableTopology X := ⊢ ∃ X x, WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ ¬FirstCountableTopology X All goals completed! 🐙

Under CH, such a space (for Problem 3 in [Ar2013]) exists as constructed in [Ya1976] by Yakovlev.

@[category research solved, AMS 54] theorem CH.existsWeaklyFirstCountableCompactNotFirstCountable [Fact (ℵ₁ = 𝔠)] : ∃ (X : Type) (_ : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ ¬ FirstCountableTopology X := inst✝:Fact (ℵ_ 1 = 𝔠)⊢ ∃ X x, WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ ¬FirstCountableTopology X All goals completed! 🐙

Problem 4 in [Ar2013]: If a Tychonoff weakly first-countable space has countable Souslin number, then does its cardinality not exceed the continuum?

@[category research open, AMS 54] theorem cardinalMk_le_continuum_of_weaklyFirstCountable_of_countableSouslinNumber : answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), T35Space X → WeaklyFirstCountableTopology X → HasCountableSouslinNumber X → #X ≤ 𝔠 := ⊢ True ↔ ∀ (X : Type) (x : TopologicalSpace X), T35Space X → WeaklyFirstCountableTopology X → HasCountableSouslinNumber X → #X ≤ 𝔠 All goals completed! 🐙end WeaklyFirstCountable