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.
A topological space is Hausdorff if and only if every net has at most one limit
Statement
A topological space is Hausdorff if and only if every net in has at most one limit.
Facts & Assumptions
Given: A topological space .
Distinct points in a Hausdorff space have disjoint neighbourhoods (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).
A net converges to a point exactly when it is eventually in each of that point's neighbourhoods (Convergence and cluster points of a net in a topological space).
Proof
Suppose is Hausdorff and a net converges to both and . If , take disjoint neighbourhoods of and of ; the net is eventually in both, and directedness supplies an index after both thresholds, whose value would lie in .
Conversely, suppose is not Hausdorff. Choose distinct for which every neighbourhood of meets every neighbourhood of , and let , ordered by reverse inclusion in the first two coordinates.
Thus , so every net has at most one limit.
The set is directed: intersect the first two neighbourhood coordinates of two triples and choose a point in their intersection; the resulting triple is above both. The net sending to is eventually in every neighbourhood of and every neighbourhood of , hence converges to both distinct points.
Therefore uniqueness of all net limits forces to be Hausdorff, and the two implications prove the result.
Depends on
- Convergence and cluster points of a net in a topological space
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 47 results over 12 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
- WVU Math 581 Topology I (standard reference, not scraped)
- Net (mathematics) (Wikipedia) (standard reference, not scraped)
- Hausdorff space (Wikipedia) (standard reference, not scraped)