LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Noetherian open subsets are quasi-compact

Statement

Assume the Axiom of Choice. Every open subset of a Noetherian topological space is quasi-compact, including the empty open subset.

Facts & Assumptions

Given: AC, a Noetherian space $X$ , an open subset $U$ , and an open cover $(U_{i})_{i \in I}$ of $U$ .

[F1]

Noetherian means every ascending sequence of open subsets stabilizes. (Noetherian topological spaces via ACC on opens or DCC on closed subsets)

[F2]

A subspace is quasi-compact when each of its open covers has a finite subcover. Since $U$ is open, its relatively open subsets are open in $X$ . (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, 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)

[A1]

AC permits the recursive selections below. (The Axiom of Choice)

Proof

1.1F2A1construct

If the cover has no finite subcover, start with $V_{0} = \emptyset$ . Given the finite union $V_{n}$ of previously selected members, choose a point of $U ∖ V_{n}$ and a cover member containing it, and let $V_{n + 1}$ be its union with $V_{n}$ . AC licenses these countably many choices. Every $V_{n}$ is open in $X$ , and $V_{n} ⊊ V_{n + 1}$ .

2.1F1F2step 1.1

This contradicts [F1]. Thus the cover has a finite subcover and $U$ is quasi-compact. For $U = \emptyset$ , the empty subcover already suffices. ∎

Depends on

Used by

A Weil divisor that is not Cartier at the vertex of the quadric cone Counterexample

Dependency tree · two levels

12 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

The Stacks Project; elementary local prerequisite for the Step 5b citation repair (standard reference, not scraped)