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)

class WeaklyFirstCountable.WeaklyFirstCountableTopology (X : Type u_1) [TopologicalSpace X] : Prop

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$

• 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

theorem WeaklyFirstCountable.exists_weakly_first_countable_not_first_countable : ∃ (X : Type) (x : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ ¬FirstCountableTopology X

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

instance WeaklyFirstCountable.FirstCountableTopology.weaklyFirstCountableTopology (X : Type u_1) [TopologicalSpace X] [FirstCountableTopology X] : WeaklyFirstCountableTopology X

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

theorem WeaklyFirstCountable.existsWeaklyFirstCountableCompactBig : True ↔ ∃ (X : Type) (x : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ Cardinal.continuum < Cardinal.mk X

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.

theorem WeaklyFirstCountable.existsWeaklyFirstCountableCompactNotFirstCountable : ∃ (X : Type) (x : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ ¬FirstCountableTopology X

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.

theorem WeaklyFirstCountable.CH.existsWeaklyFirstCountableCompactNotFirstCountable [Fact (Cardinal.aleph 1 = Cardinal.continuum)] : ∃ (X : Type) (x : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧ ¬FirstCountableTopology X

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