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 finite simplicial complex has a compact Hausdorff realization
Statement
If is a finite abstract simplicial complex, then its geometric realization is compact and Hausdorff.
Facts & Assumptions
Given: A finite abstract simplicial complex .
There are finitely many simplices, and the realization has barycentric coordinates and the weak topology determined by their Euclidean simplex topologies (Local finiteness, finiteness, and finite dimensionality of a simplicial complex, The geometric realization of an abstract simplicial complex).
Closed subsets of a subspace are traces of ambient closed sets. In particular, a closed subset of a closed subspace is ambient closed (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). Finite unions of closed sets are closed by complementation of finite intersections of open sets (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).
A closed bounded subset of Euclidean , for , is compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line); distinct points have disjoint open metric balls (Distinct points of a metric space have disjoint balls around them).
Proof
If there is no nonempty simplex, the realization is empty and is compact and Hausdorff. Otherwise enumerate the finitely many vertices as , with . The barycentric coordinate map identifies the realization as a set with , where On each simplex this identification has precisely its Euclidean simplex topology.
Each is closed in . Indeed coordinates and their sum are continuous: and . Thus violating any of its finitely many closed coordinate constraints persists on a sufficiently small ball. The finite union is closed by [L2] and bounded since it lies in .
A subset is weakly closed exactly when is closed in for every nonempty simplex, by taking complements in the weak-open criterion [L1]. If is weakly closed, each such intersection is closed in by step 2.1 and [L2]. Their finite union is , so is closed in . Conversely, if is closed in , all its traces on are closed there by [L2], hence is weakly closed. Therefore the weak topology equals the Euclidean subspace topology on .
By [L3] and step 2.1, is compact. For two distinct points of , intersect their disjoint Euclidean open balls from [L3] with ; these are disjoint subspace-open neighborhoods. Hence is Hausdorff. Step 3.1 transfers both properties to the realization; step 1.1 handled the empty case.
Depends on
The geometric realization of an abstract simplicial complex
Local finiteness, finiteness, and finite dimensionality of a simplicial complex
Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
Distinct points of a metric space have disjoint balls around them