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 Cardinal namespace WeaklyFirstCountable

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

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

@[category textbook, AMS 54] theorem declaration uses 'sorry'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$.

@[category test, AMS 54] instance FirstCountableTopology.weaklyFirstCountableTopology (X : Type*) [TopologicalSpace X] [FirstCountableTopology X] : WeaklyFirstCountableTopology X := X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology X⊢ WeaklyFirstCountableTopology X have has_basis: ∀ a : X, ∃ x : ℕ → Set X, (𝓝 a).HasAntitoneBasis x := X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology X⊢ WeaklyFirstCountableTopology X X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xa:X⊢ ∃ x, (𝓝 a).HasAntitoneBasis x X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xa:X⊢ (𝓝 a).IsCountablyGenerated All goals completed! 🐙 X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choose⊢ WeaklyFirstCountableTopology X X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)⊢ WeaklyFirstCountableTopology X X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)⊢ (∀ (x : X), Antitone (U x) ∧ ∀ (n : ℕ), x ∈ U x n) ∧ ∀ (O : Set X), IsOpen O ↔ ∀ x ∈ O, ∃ k, U x k ⊆ O X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)⊢ ∀ (x : X), Antitone (U x) ∧ ∀ (n : ℕ), x ∈ U x nX:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)⊢ ∀ (O : Set X), IsOpen O ↔ ∀ x ∈ O, ∃ k, U x k ⊆ O X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)⊢ ∀ (x : X), Antitone (U x) ∧ ∀ (n : ℕ), x ∈ U x n All goals completed! 🐙 X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)O:Set X⊢ IsOpen O ↔ ∀ x ∈ O, ∃ k, U x k ⊆ O X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)O:Set X⊢ (∀ x ∈ O, ∃ k, U x k ⊆ O) → ∀ x ∈ O, O ∈ 𝓝 x intro h X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)O:Set Xh:∀ x ∈ O, ∃ k, U x k ⊆ Ox:X⊢ x ∈ O → O ∈ 𝓝 x X:Type u_1inst✝¹:TopologicalSpace Xinst✝:FirstCountableTopology Xhas_basis:∀ (a : X), ∃ x, (𝓝 a).HasAntitoneBasis x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis 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 x := fun a => Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext isCountablyGenerated_iff_exists_antitone_basis)))) (FirstCountableTopology.nhds_generated_countable a)U:X → ℕ → Set X := fun x => ⋯.choosehU:∀ (x : X), (𝓝 x).HasAntitoneBasis (U x) := fun x => Exists.choose_spec (has_basis x)O:Set Xh:∀ x ∈ O, ∃ k, U x k ⊆ Ox:Xhx:x ∈ On:ℕhn:U x n ⊆ O⊢ O ∈ 𝓝 x 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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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! 🐙 -- TODO: add Problem 4 in [Ar2013] end WeaklyFirstCountable