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.
Dimension of a finite closed union
Statement
If a Noetherian space is a finite union of closed subsets , then . For both sides are .
Facts & Assumptions
Given: The objects and hypotheses in the statement.
For a Noetherian topological space , define as the supremum of the lengths of strict chains of nonempty irreducible closed subsets of . Thus a one-member chain has length zero. Set , and allow . The supremum of an empty family of dimensions is . (Chain dimension and the empty-space convention).
Proof
If or , there are no nonempty irreducible closed subsets and the conventions give the equality. Otherwise every chain in a closed is also a chain in , giving .
For a chain in , write . Irreducibility, applied repeatedly to this finite closed cover, forces for some . The entire chain lies in that . Taking suprema gives the reverse bound, including unbounded chain lengths.