WeaklyFirstCountable.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

11 declarations, 5 contain sorry, 0 declared as axioms

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)

Imports (1)

FormalConjecturesUtil

class WeaklyFirstCountable.WeaklyFirstCountableTopology A topological space line 51 source
Source documentation
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$
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace
```
class WeaklyFirstCountableTopology (X : Type*) [TopologicalSpace X] : Prop where
…
```
def WeaklyFirstCountable.IsCellularFamily A cellular family is a pairwise-disjoint collection of nonempty open sets line 58 source
Source documentation
A cellular family is a pairwise-disjoint collection of nonempty open sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Set
Proof uses: And, Set.PairwiseDisjoint, id, Membership.mem, IsOpen, Set.Nonempty
7 instances, coercions and auxiliary constants left out.
```
def IsCellularFamily (X : Type u) [TopologicalSpace X] (F : Set (Set X)) : Prop :=
…
```
def WeaklyFirstCountable.souslinNumber The Souslin number of a topological space is the supremum of the cardinalities of its cellular families line 63 source
Source documentation
The Souslin number of a topological space is the supremum of the cardinalities of its cellular families.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Cardinal
Proof uses: iSup, Subtype, Set, WeaklyFirstCountable.IsCellularFamily, Cardinal.mk
8 instances, coercions and auxiliary constants left out.
```
noncomputable def souslinNumber (X : Type u) [TopologicalSpace X] : Cardinal.{u} :=
…
```
class WeaklyFirstCountable.HasCountableSouslinNumber A space has countable Souslin number when its Souslin number is at most ℵ₀ line 67 source
Source documentation
A space has countable Souslin number when its Souslin number is at most ℵ₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace
```
class HasCountableSouslinNumber (X : Type u) [TopologicalSpace X] : Prop where
…
```
theorem WeaklyFirstCountable.exists_weakly_first_countable_not_first_countable There are weakly first countable spaces which are not first countable, for example the Arens Space sorry line 73 source
Source documentation
There are weakly first countable spaces which are not first countable, for example the Arens Space.

L4DEL explanation
There are weakly first countable spaces which are not first countable, for example the Arens Space.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Exists, TopologicalSpace, And, WeaklyFirstCountable.WeaklyFirstCountableTopology, Not, FirstCountableTopology
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_weakly_first_countable_not_first_countable : ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ ¬ FirstCountableTopology X := by sorry
…
```
Mentions: WeaklyFirstCountable.WeaklyFirstCountableTopology
instance WeaklyFirstCountable.FirstCountableTopology.weaklyFirstCountableTopology Every first countable space is weakly first countable, simply take $N x$ as a countable neighborhood basis of $x$ line 79 source
Source documentation
Every first countable space is weakly first countable, simply take $N x$ as a countable neighborhood basis of $x$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, FirstCountableTopology, WeaklyFirstCountable.WeaklyFirstCountableTopology
Proof uses: Exists, Nat, Set, Filter.HasAntitoneBasis, nhds, Eq.mpr, Filter.IsCountablyGenerated, id, Eq, congrArg, Eq.symm, propext, Filter.isCountablyGenerated_iff_exists_antitone_basis, Exists.choose, Exists.choose_spec, WeaklyFirstCountable.WeaklyFirstCountableTopology.mk, Exists.intro, And, Antitone, Membership.mem and 13 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
instance FirstCountableTopology.weaklyFirstCountableTopology (X : Type*) [TopologicalSpace X]
    [FirstCountableTopology X] : WeaklyFirstCountableTopology X := by
…
```
Mentions: WeaklyFirstCountable.WeaklyFirstCountableTopology
instance WeaklyFirstCountable.hasCountableSouslinNumber_of_separable Every separable space has countable Souslin number line 100 source
Source documentation
Every separable space has countable Souslin number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, TopologicalSpace.SeparableSpace, WeaklyFirstCountable.HasCountableSouslinNumber
Proof uses: WeaklyFirstCountable.HasCountableSouslinNumber.mk, ciSup_le', Cardinal, Subtype, Set, WeaklyFirstCountable.IsCellularFamily, Cardinal.mk, Cardinal.aleph0, Set.Countable.le_aleph0, Set.PairwiseDisjoint.countable_of_isOpen, id, And.left, Set.PairwiseDisjoint, Membership.mem, And, IsOpen, Set.Nonempty, Subtype.property, And.right
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
instance hasCountableSouslinNumber_of_separable (X : Type u) [TopologicalSpace X]
    [SeparableSpace X] : HasCountableSouslinNumber X where
…
```
Mentions: WeaklyFirstCountable.HasCountableSouslinNumber
theorem WeaklyFirstCountable.existsWeaklyFirstCountableCompactBig Problem 2 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space X such that $𝔠 < |X|$ sorry line 114 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, True, Exists, TopologicalSpace, And, WeaklyFirstCountable.WeaklyFirstCountableTopology, CompactSpace, T2Space, LT.lt, Cardinal, Cardinal.continuum, Cardinal.mk
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem existsWeaklyFirstCountableCompactBig : answer(sorry) ↔
    ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧
        𝔠 < #X := by
…
```
Mentions: WeaklyFirstCountable.WeaklyFirstCountableTopology
theorem WeaklyFirstCountable.existsWeaklyFirstCountableCompactNotFirstCountable Problem 3 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space which is not first countable sorry line 126 source
Source documentation
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.

depends on sorry what this means
Statement uses: Exists, TopologicalSpace, And, WeaklyFirstCountable.WeaklyFirstCountableTopology, CompactSpace, T2Space, Not, FirstCountableTopology
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem existsWeaklyFirstCountableCompactNotFirstCountable :
    ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧
        ¬ FirstCountableTopology X := by
…
```
Mentions: WeaklyFirstCountable.WeaklyFirstCountableTopology
theorem WeaklyFirstCountable.CH.existsWeaklyFirstCountableCompactNotFirstCountable Under CH, such a space (for Problem 3 in [Ar2013]) exists as constructed in [Ya1976] by Yakovlev sorry line 135 source
Source documentation
Under CH, such a space (for Problem 3 in [Ar2013]) exists as constructed in [Ya1976] by Yakovlev.

depends on sorry what this means
Statement uses: Fact, Eq, Cardinal, OrderEmbedding, Ordinal, Cardinal.aleph, OfNat.ofNat, Cardinal.continuum, Exists, TopologicalSpace, And, WeaklyFirstCountable.WeaklyFirstCountableTopology, CompactSpace, T2Space, Not, FirstCountableTopology
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem CH.existsWeaklyFirstCountableCompactNotFirstCountable
    [Fact (ℵ₁ = 𝔠)] :
    ∃ (X : Type) (_ : TopologicalSpace X),
      WeaklyFirstCountableTopology X ∧ CompactSpace X ∧ T2Space X ∧
        ¬ FirstCountableTopology X := by sorry
…
```
Mentions: WeaklyFirstCountable.WeaklyFirstCountableTopology
theorem WeaklyFirstCountable.cardinalMk_le_continuum_of_weaklyFirstCountable_of_countableSouslinNumber Problem 4 in [Ar2013]: If a Tychonoff weakly first-countable space has countable Souslin number, then does its cardinality not exceed the continuum? sorry line 144 source
Source documentation
Problem 4 in [Ar2013]: If a Tychonoff weakly first-countable space has countable Souslin number, then does its cardinality not exceed the continuum?

depends on sorry what this means
Statement uses: Iff, True, TopologicalSpace, T35Space, WeaklyFirstCountable.WeaklyFirstCountableTopology, WeaklyFirstCountable.HasCountableSouslinNumber, LE.le, Cardinal, Cardinal.mk, Cardinal.continuum
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cardinalMk_le_continuum_of_weaklyFirstCountable_of_countableSouslinNumber :
    answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), T35Space X →
      WeaklyFirstCountableTopology X → HasCountableSouslinNumber X → #X ≤ 𝔠 := by
…
```
Mentions: WeaklyFirstCountable.WeaklyFirstCountableTopology, WeaklyFirstCountable.HasCountableSouslinNumber