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
- Under choice, every regular T₁ second-countable space is metrizable Corollary
- 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
- Every discrete family is locally finite, so every σ-discrete basis is σ-locally finite Lemma
- Under choice, every metric space has a σ-locally-finite basis Lemma
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 30 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Encyclopedia of Mathematics, Metrizable space (standard reference, not scraped)