CardinalInvariants.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

24 declarations, 0 contain sorry, 0 declared as axioms

Cardinal invariants of topological spaces

This file defines networks of a topological space and two cardinal invariants: the density d(X) and the network weight nw(X). As usual, both are made infinite by adding ℵ₀, following the convention for cardinal invariants in Felix Pernegger's pibase-lean (PiBaseLean/AdditionalDefs/Cardinal.lean).

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

def TopologicalSpace.IsNetwork A family N of subsets of a topological space X is a network for X if every open subset of X is a union of members of N line 44 source
Source documentation
A family N of subsets of a topological space X is a network for X if every open subset of X is a union of members of N. Unlike the members of a topological basis, the members of a network need not be open.

no axioms what this means
Statement uses: TopologicalSpace, Set
Proof uses: IsOpen, Membership.mem, Exists, And, LE.le
2 instances, coercions and auxiliary constants left out.
```
def IsNetwork (N : Set (Set X)) : Prop :=
…
```
theorem TopologicalSpace.IsTopologicalBasis.isNetwork line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Set, TopologicalSpace.IsTopologicalBasis, TopologicalSpace.IsNetwork
Proof uses: IsOpen, Membership.mem, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
1 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace.isNetwork_setOf_isOpen line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, TopologicalSpace.IsNetwork, Set.ofPred, Set, IsOpen
Proof uses: TopologicalSpace.IsTopologicalBasis.isNetwork, TopologicalSpace.isTopologicalBasis_opens
theorem TopologicalSpace.IsNetwork.preimage The preimage of a network under an inducing map is a network line 55 source
Source documentation
The preimage of a network under an inducing map is a network.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Set, TopologicalSpace.IsNetwork, Topology.IsInducing, Set.image, Set.preimage
Proof uses: IsOpen, Membership.mem, And, Eq, Exists, LE.le, Iff.mp, Topology.IsInducing.isOpen_iff, Exists.intro, And.intro, Set.mem_image_of_mem, Set.preimage_mono
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem IsNetwork.preimage {N : Set (Set Y)} (hN : IsNetwork N) {f : X → Y}
    (hf : IsInducing f) : IsNetwork ((f ⁻¹' ·) '' N) := by
…
```
Mentions: TopologicalSpace.IsNetwork
def TopologicalSpace.density The density d(X) of a topological space X: the least cardinality of a dense subset, plus ℵ₀ line 66 source
Source documentation
The density d(X) of a topological space X: the least cardinality of a dense subset, plus ℵ₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Cardinal
Proof uses: HAdd.hAdd, iInf, Subtype, Set, Dense, Cardinal.mk, Cardinal.aleph0
10 instances, coercions and auxiliary constants left out.
```
noncomputable def density : Cardinal :=
…
```
def TopologicalSpace.networkWeight The network weight nw(X) of a topological space X: the least cardinality of a network, plus ℵ₀ line 71 source
Source documentation
The network weight nw(X) of a topological space X: the least cardinality of a network, plus ℵ₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Cardinal
Proof uses: HAdd.hAdd, iInf, Subtype, Set, TopologicalSpace.IsNetwork, Cardinal.mk, Cardinal.aleph0
10 instances, coercions and auxiliary constants left out.
```
noncomputable def networkWeight : Cardinal :=
…
```
instance TopologicalSpace.(instance at line 76) line 76 source
instance TopologicalSpace.(instance at line 78) line 78 source
theorem TopologicalSpace.aleph0_le_density line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, LE.le, Cardinal, Cardinal.aleph0, TopologicalSpace.density
Proof uses: le_add_self, iInf, Subtype, Set, Dense, Cardinal.mk
12 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace.aleph0_le_networkWeight line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, LE.le, Cardinal, Cardinal.aleph0, TopologicalSpace.networkWeight
Proof uses: le_add_self, iInf, Subtype, Set, TopologicalSpace.IsNetwork, Cardinal.mk
12 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace._root_.Dense.density_le line 84 source
theorem TopologicalSpace.IsNetwork.networkWeight_le line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Set, TopologicalSpace.IsNetwork, LE.le, Cardinal, TopologicalSpace.networkWeight, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0
Proof uses: add_le_add_left, iInf, Subtype, Subtype.mk, ciInf_le'
18 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace.density_le_mk_add_aleph0 line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, LE.le, Cardinal, TopologicalSpace.density, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0
Proof uses: LE.le.trans_eq, Set.univ, Dense.density_le, dense_univ, Eq.mpr, Eq, id, congrArg, Cardinal.mk_univ, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TopologicalSpace.isNetwork_range_sInter The sets ⋂₀ {U | IsOpen U ∧ x ∈ U}, for x : X, form a network of X line 95 source
Source documentation
The sets ⋂₀ {U | IsOpen U ∧ x ∈ U}, for x : X, form a network of X.

no axioms what this means
Statement uses: TopologicalSpace, TopologicalSpace.IsNetwork, Set.range, Set, Set.sInter, Set.ofPred, And, IsOpen, Membership.mem
Proof uses: Exists.intro, LE.le, And.intro, Set.mem_range_self, And.right
3 instances, coercions and auxiliary constants left out.
```
theorem isNetwork_range_sInter : IsNetwork (range fun x : X => ⋂₀ {U | IsOpen U ∧ x ∈ U}) :=
…
```
Mentions: TopologicalSpace.IsNetwork
theorem TopologicalSpace.networkWeight_le_mk_add_aleph0 line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, LE.le, Cardinal, TopologicalSpace.networkWeight, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0
Proof uses: LE.le.trans, Set, Set.range, Set.sInter, Set.ofPred, And, IsOpen, Membership.mem, TopologicalSpace.IsNetwork.networkWeight_le, TopologicalSpace.isNetwork_range_sInter, add_le_add_left, Cardinal.mk_range_le
11 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace.exists_dense_mk_add_aleph0_eq_density The density is attained by some dense subset line 102 source
Source documentation
The density is attained by some dense subset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Exists, Set, And, Dense, Eq, Cardinal, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0, TopologicalSpace.density
Proof uses: Membership.mem, Set.range, Subtype, iInf, ciInf_mem, Subtype.mk, Exists.intro, And.intro, congrArg
17 instances, coercions and auxiliary constants left out.
```
theorem exists_dense_mk_add_aleph0_eq_density : ∃ s : Set X, Dense s ∧ #s + ℵ₀ = density X :=
…
```
Mentions: TopologicalSpace.density
theorem TopologicalSpace.exists_isNetwork_mk_add_aleph0_eq_networkWeight The network weight is attained by some network line 107 source
Source documentation
The network weight is attained by some network.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Exists, Set, And, TopologicalSpace.IsNetwork, Eq, Cardinal, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0, TopologicalSpace.networkWeight
Proof uses: Membership.mem, Set.range, Subtype, iInf, ciInf_mem, Subtype.mk, Exists.intro, And.intro, congrArg
17 instances, coercions and auxiliary constants left out.
```
theorem exists_isNetwork_mk_add_aleph0_eq_networkWeight :
    ∃ N : Set (Set X), IsNetwork N ∧ #N + ℵ₀ = networkWeight X :=
…
```
Mentions: TopologicalSpace.IsNetwork, TopologicalSpace.networkWeight
theorem TopologicalSpace.le_density line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Cardinal, Set, Dense, LE.le, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0, TopologicalSpace.density
Proof uses: Exists, And, Eq, TopologicalSpace.exists_dense_mk_add_aleph0_eq_density, Eq.rec
9 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace.le_networkWeight line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Cardinal, Set, TopologicalSpace.IsNetwork, LE.le, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0, TopologicalSpace.networkWeight
Proof uses: Exists, And, Eq, TopologicalSpace.exists_isNetwork_mk_add_aleph0_eq_networkWeight, Eq.rec
9 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace.density_le_aleph0_iff line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Iff, LE.le, Cardinal, TopologicalSpace.density, Cardinal.aleph0, TopologicalSpace.SeparableSpace
Proof uses: Iff.intro, Set, And, Dense, Eq, HAdd.hAdd, Cardinal.mk, Exists, TopologicalSpace.exists_dense_mk_add_aleph0_eq_density, TopologicalSpace.SeparableSpace.mk, Exists.intro, Set.Countable, And.intro, Iff.mp, Countable, Set.countable_coe_iff, Cardinal.mk_le_aleph0_iff, LE.le.trans, le_self_add, Eq.trans_le and 6 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem TopologicalSpace.networkWeight_le_aleph0 line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, SecondCountableTopology, LE.le, Cardinal, TopologicalSpace.networkWeight, Cardinal.aleph0
Proof uses: Exists, Set, And, Set.Countable, Not, Membership.mem, EmptyCollection.emptyCollection, TopologicalSpace.IsTopologicalBasis, TopologicalSpace.exists_countable_basis, LE.le.trans, HAdd.hAdd, Cardinal.mk, TopologicalSpace.IsNetwork.networkWeight_le, TopologicalSpace.IsTopologicalBasis.isNetwork, LE.le.trans_eq, add_le_add_left, Iff.mpr, Countable, Cardinal.mk_le_aleph0_iff, Set.Countable.to_subtype and 1 more
11 instances, coercions and auxiliary constants left out.
theorem TopologicalSpace._root_.Topology.IsInducing.networkWeight_le The network weight of a subspace is at most that of the ambient space line 137 source
Source documentation
The network weight of a subspace is at most that of the ambient space.
```
theorem _root_.Topology.IsInducing.networkWeight_le {X Y : Type u} [TopologicalSpace X]
    [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) :
    networkWeight X ≤ networkWeight Y :=
…
```
Mentions: TopologicalSpace.networkWeight
theorem TopologicalSpace.density_discrete line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, DiscreteTopology, Eq, Cardinal, TopologicalSpace.density, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0
Proof uses: le_antisymm, TopologicalSpace.density_le_mk_add_aleph0, TopologicalSpace.le_density, Set, Dense, Set.univ, LE.le, Eq.mpr, id, congrArg, Cardinal.mk_univ, le_refl, Eq.symm, Iff.mp, dense_discrete
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem TopologicalSpace.networkWeight_discrete line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, DiscreteTopology, Eq, Cardinal, TopologicalSpace.networkWeight, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0
Proof uses: le_antisymm, TopologicalSpace.networkWeight_le_mk_add_aleph0, TopologicalSpace.le_networkWeight, Set, TopologicalSpace.IsNetwork, Membership.mem, Singleton.singleton, And, LE.le, Exists, isOpen_discrete, rfl, Eq.mp, congrArg, subset_antisymm, Iff.mpr, Set.singleton_subset_iff, add_le_add_left, Subtype, Cardinal.mk_le_of_injective and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.