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.
Assuming the ultrafilter lemma, every Tychonoff space has a Hausdorff compactification
Statement
Assume the ultrafilter lemma. If is Tychonoff, is its full evaluation map, and , then is a Hausdorff compactification of . In particular every Tychonoff space has one. This statement uses the ultrafilter lemma only for compactness of the cube; it makes no assertion about dependent choice.
Facts & Assumptions
Given: A Tychonoff space and the ultrafilter lemma.
Assuming the ultrafilter lemma, every product of compact Hausdorff spaces is compact (Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact).
A closed subspace of a compact space is compact, and a point lies in the closure of exactly when every open neighbourhood of it meets (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, A point lies in the closure of iff every basic neighbourhood of it meets ; the closure is the smallest closed superset and equals together with its derived set).
A Tychonoff space embeds in a unit cube (A space is Tychonoff if and only if it embeds in a cube ).
An arbitrary product of Hausdorff spaces is Hausdorff (Arbitrary products preserve , , and Hausdorffness).
The interval is compact, and its usual metric topology is Hausdorff (Heine-Borel by bisection: every closed bounded interval is compact, Distinct points of a metric space have disjoint balls around them).
Proof
By [L3], the full evaluation map embeds as in the cube . By [L5] the interval is compact Hausdorff, so [L1] makes compact and [L4] makes it Hausdorff.
Put . It is closed, hence compact by [L2], and it is Hausdorff as a subspace of the Hausdorff space .
The evaluation embedding has image , which is dense in by the definition of closure and [L2]. Thus is a Hausdorff compactification in the sense of A Hausdorff compactification as a dense embedding into a compact Hausdorff space.
Depends on
- A space is Tychonoff if and only if it embeds in a cube $[0,1]^J$
- A Hausdorff compactification as a dense embedding into a compact Hausdorff space
- Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact
- Arbitrary products preserve $T_0$, $T_1$, and Hausdorffness
- A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
- A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$; the closure is the smallest closed superset and equals $A$ together with its derived set
- Heine-Borel by bisection: every closed bounded interval $[a,b]$ is compact
- Distinct points of a metric space have disjoint balls around them
Used by
- Under the ultrafilter lemma and dependent choice, the closure of the full evaluation image is the Stone–Čech compactification Theorem
- Under the ultrafilter lemma and the Axiom of Choice, every completely metrizable space is Čech-complete Theorem
- Under the ultrafilter lemma, every metrizable Čech-complete space is completely metrizable Theorem
Dependency tree · two levels
55 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
- E. Moorhouse, The Stone–Čech Compactification (standard reference, not scraped)