Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Discrete families and -locally-finite and -discrete bases
Definition
Let be a topological space. A family of subsets of is discrete if every has a neighbourhood meeting at most one member of . It is therefore a locally finite family in the sense of Refinements, locally finite families, point-finite families, and star refinements.
An open basis (Basis and subbasis for a topology, and the topology generated by a family of sets) is -locally finite if for locally finite families , and -discrete if the families can be taken discrete. Empty layers are permitted; the word records the countable indexing convention of Finite, countably infinite, countable, uncountable.
Depends on
Used by
- Normalized families and collectionwise normality Definition
- An uncountable discrete space is metrizable and has a discrete basis, but is not second countable Example
- A locally finite open cover by subspaces with σ-locally-finite bases yields a σ-locally-finite basis of the whole space Lemma
- A sigma-cellular base metrizes a normal Moore space Lemma
- Collectionwise normal Moore spaces are screenable Lemma
- Every discrete family is locally finite, so every σ-discrete basis is σ-locally finite Lemma
- Metrizable spaces are collectionwise normal Lemma
- The PMEA three-quarter separation estimate Lemma
- Under choice, every metric space has a σ-locally-finite basis Lemma
- Collectionwise normal Moore spaces are metrizable Theorem
- Fleissner's construction of a normal nonmetrizable Moore space from level data Theorem
- Moore spaces are subparacompact Theorem
- Normal screenable Moore spaces are metrizable Theorem
- PMEA makes normal low-character spaces collectionwise normal Theorem
Dependency tree · two levels
11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Encyclopedia of Mathematics, Metrizable space (standard reference, not scraped)