LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)

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.

The graph of a continuous map into a Hausdorff space is closed in the product

Statement

Let $X$ be a topological space, let $Y$ be Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) and let $f : X \to Y$ be continuous (Continuity of a map of topological spaces at a point and globally). Then the graph

$G_{f} : = {z \in X \times Y : z_{1} = f (z_{0})} = {(x, f (x)) : x \in X}$

is closed in $X \times Y$ with the product topology (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).

No hypothesis is placed on $X$ . The Hausdorff hypothesis is on the codomain and the continuity hypothesis is on $f$ ; both are used, and the converse implication — that a closed graph forces continuity — needs a different hypothesis on the codomain and is treated separately.

Facts & Assumptions

Given: A topological space $X$ , a Hausdorff space $Y$ , a continuous map $f : X \to Y$ , and the product $X \times Y$ with the product topology and projections $π_{0}, π_{1}$ .

[A1]

$G_{f} = {z \in X \times Y : (f \circ π_{0}) (z) = π_{1} (z)}$ , since $(f \circ π_{0}) (z) = f (z_{0})$ and $π_{1} (z) = z_{1}$ (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, The diagonal $Δ_{X} \subseteq X \times X$ , the diagonal map $δ_{X}$ , and the pairing $⟨ f, g ⟩$ of two maps).

[L1]

The projections $π_{0} : X \times Y \to X$ and $π_{1} : X \times Y \to Y$ are continuous (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, claim 1).

[L2]

A composite of continuous maps is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1).

[L3]

If $Y$ is Hausdorff and $u, v : Z \to Y$ are continuous, then ${z \in Z : u (z) = v (z)}$ is closed in $Z$ (For continuous $f, g : Z \to Y$ with $Y$ Hausdorff the agreement set ${z \in Z : f (z) = g (z)}$ is closed in $Z$ , Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Proof

technique · direct

1.1

$π_{0}$ and $π_{1}$ are continuous.

2.1

$f \circ π_{0} : X \times Y \to Y$ is continuous, being a composite of the continuous $π_{0}$ with the continuous $f$ .

step 1.1L2

3.1

By [A1] the graph $G_{f}$ is the agreement set of the two continuous maps $f \circ π_{0}$ and $π_{1}$ from $X \times Y$ to the Hausdorff space $Y$ , so it is closed in $X \times Y$ .

step 1.1step 2.1A1L3∎

Remarks

The graph is an agreement set, and that is the whole proof. Writing $G_{f}$ as the set where $f \circ π_{0}$ and $π_{1}$ agree turns a statement about a map into a statement about two maps out of one space, which is exactly the shape For continuous $f, g : Z \to Y$ with $Y$ Hausdorff the agreement set ${z \in Z : f (z) = g (z)}$ is closed in $Z$ handles. Equivalently $G_{f} = ⟨ f \circ π_{0}, π_{1} ⟩^{- 1} [Δ_{Y}]$ , the preimage of the diagonal (The diagonal $Δ_{X} \subseteq X \times X$ , the diagonal map $δ_{X}$ , and the pairing $⟨ f, g ⟩$ of two maps).
The Hausdorff hypothesis is not removable. Let $X$ be a one-point space and let $Y = {a, b}$ with $a \neq b$ carry the indiscrete topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies). Every function $X \to Y$ is continuous, the only preimages to check being those of $\emptyset$ and $Y$ . The product $X \times Y$ has as its open boxes only $\emptyset$ and itself, so its only closed sets are $\emptyset$ and itself; and $G_{f}$ is a single point, hence neither. The argument above breaks at [L3] and nowhere else.
Continuity of $f$ is used, and only through the composite. Step 2.1 is the only appearance of the hypothesis; everything else is a property of the product.

Depends on

Used by

Dependency tree · two levels

25 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

Hausdorff space (Wikipedia) (standard reference, not scraped)
Closed graph theorem (Wikipedia) (standard reference, not scraped)
Stacks Project, Topology, Lemma 5.3 (Tag 08ZD) (standard reference, not scraped)