How 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.
First countable space: a countable neighbourhood base at every point
Definition
A topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) is first countable if every point of has an at most countable neighbourhood base: for each there is a family that is at most countable (Finite, countably infinite, countable, uncountable, Equinumerous sets, and ) and such that every neighbourhood of contains a member of (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).
"Countable" here means "at most countable", as everywhere in this library (Finite, countably infinite, countable, uncountable), so a finite neighbourhood base is permitted. That is not a degenerate case: in a discrete space the one-element family is a neighbourhood base at , so every discrete space is first countable, and in an indiscrete space is a neighbourhood base at every point.
The base may be taken to consist of open sets, and it may be taken decreasing. If is an at most countable neighbourhood base at , then replacing each by an open with gives an at most countable neighbourhood base of open sets. Making the base decreasing, that is arranging , requires enumerating it and forming the running finite intersections; both operations are carried out inside the proof of the theorem that uses them, the next item, where the enumeration and the recursion are cited explicitly rather than assumed here.
First countability is a topological property (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological): a homeomorphism carries a neighbourhood base at to a neighbourhood base at , since is a bijection between the neighbourhood filters preserving inclusion, and a bijection preserves at most countability (Equinumerous sets, and ).
Remarks
-
What first countability buys. Under countable choice, it is a sufficient hypothesis under which sequences detect the topology: the closure is the sequential closure and sequential continuity is continuity. It is not necessary: the later hierarchy Assuming countable choice, every first countable space is Fréchet–Urysohn; in ZF every Fréchet–Urysohn space is sequential ↗ distinguishes first countable, Fréchet--Urysohn, and sequential spaces. Without an additional hypothesis sequences can be too weak. Under that same choice assumption, both failures occur in the cocountable topology on , so the cited implication shows that space is not first countable.
-
Every metric space is first countable, the balls of radius for forming an at most countable neighbourhood base at each point (The balls , , form a countable neighbourhood base at , so every metric space is first countable); so every metrizable space is first countable, and a space that is not first countable is not metrizable. That is a second obstruction to metrizability, and it is not stronger than the Hausdorff obstruction used elsewhere on this page: the indiscrete topology on two points is first countable, as the paragraph above records, and is not Hausdorff, so it is caught by the Hausdorff obstruction and not by this one. The converse failure does occur under the ultrafilter lemma and countable choice: with those hypotheses, the later Cantor-cube example Assuming the Ultrafilter Lemma and Countable Choice, an uncountable Cantor cube is compact Hausdorff and uniformizable but not first countable, hence not metrizable ↗ is compact Hausdorff and not first countable. Together with the indiscrete example, this shows under those hypotheses that neither first countability nor Hausdorffness implies the other.
-
Second countability is not developed at this point in the reading order. The stronger axiom, an at most countable basis for the whole topology, is defined later in Second countability: an at most countable basis for the topology ↗. Nothing below uses it.
Depends on
- Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
- Finite, countably infinite, countable, uncountable
- Equinumerous sets, $A \approx B$ and $A \preceq B$
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological
Used by
- Every subspace of a metrizable space is metrizable and every subspace of a first countable space is first countable, the metric case being the subspace metric already identified with the subspace topology Corollary
- Under choice, the five cardinal functions recover first countability, second countability, separability, Lindelöfness, and ccc at the ℵ₀ threshold Corollary
- Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not Definition
- Assuming countable choice, ω₁ is first countable and countably compact but is not separable or Lindelöf Example
- Assuming the Ultrafilter Lemma and Countable Choice, an uncountable Cantor cube is compact Hausdorff and uniformizable but not first countable, hence not metrizable Example
- The one-point compactification of the discrete real line is compact and Lindelöf but is neither first countable nor separable Example
- The sequential fan is Fréchet–Urysohn and not first countable Example
- The Sorgenfrey line: ℝ with the half-open intervals [a,b) as a basis is strictly finer than the usual topology, is first countable, has a countable dense subset, and its sequences converge only from the right Example
- FALSE: the compact-open topology on C(X,Y) is metrizable for every metric X and Y False statement
- Refuted: every first countable space is second countable False statement
- A countable local base can be chosen open and decreasing Lemma
- The four live convention forks of general topology and which side this library takes on each Remark
- Assuming countable choice, a countable product of first countable spaces is first countable Theorem
- Assuming Countable Choice, in a first countable space sequential closure equals closure and sequential continuity at a point equals continuity there Theorem
- Every second countable space is first countable Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 34 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
- First-countable space (Wikipedia) (standard reference, not scraped)
- J. Munkres, Topology, 2nd ed., §30 (standard reference, not scraped)