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.
Arbitrary products preserve , , and Hausdorffness
Statement
For any family , if every is , respectively , respectively Hausdorff, then is respectively , , respectively Hausdorff. The empty product is included.
Facts & Assumptions
Given: A family of spaces with the indicated separation property and two distinct points of its product .
Distinct product points differ at a coordinate, and is open whenever is open in (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).
The , , and Hausdorff conditions are respectively the stated one-sided, two-sided, and disjoint-open separations of distinct points ( (Kolmogorov) and (Frechet) spaces, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).
Proof
If , the product has one point and all three conditions hold vacuously.
Otherwise choose with . For a factor, the inverse image under of an open set distinguishing distinguishes .
For a factor, pull back the two open sets separating from and from .
For a Hausdorff factor, pull back disjoint open neighbourhoods of ; their inverse images remain disjoint.
Thus the product has the relevant property in every case.
Depends on
- The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space
- A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice
- $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
Used by
- Assuming the ultrafilter lemma, every Tychonoff space has a Hausdorff compactification Corollary
- Assuming choice, two paracompact lower-limit lines can have a nonparacompact product Counterexample
- Assuming the Ultrafilter Lemma and Countable Choice, an uncountable Cantor cube is compact Hausdorff and uniformizable but not first countable, hence not metrizable Example
- Assuming choice, refuted: paracompactness is productive False statement
- A space is Tychonoff if and only if it embeds in a cube [0,1]^J Theorem
- T₀, T₁, T₂, regularity, T₃, complete regularity, and Tychonoffness are productive Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 60 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
- J. P. May, An Outline Summary of Basic Point Set Topology, §6 (standard reference, not scraped)
- Separation axiom (Wikipedia) (standard reference, not scraped)