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.
Open cover, subcover, compact subset of (every open cover has a finite subcover), and sequentially compact subset
Definition
Let , with open sets as in Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen.
- An open cover of is a family of open subsets of with .
- A subcover of is a subfamily that is still an open cover of .
- A subfamily is finite when or there are and members of with ; repetitions in the list are allowed and harmless.
- is compact when every open cover of has a finite subcover: for every open cover of , either and the empty subfamily covers it, or there are and with
- is sequentially compact when every sequence of reals with for all (Sequences of reals: bounded, eventually, frequently, tails, subsequences) has a subsequence converging (Limits and Cauchy sequences of reals) to some point of ; equivalently, when every such sequence has a subsequential limit (Subsequential limit of a real sequence, and the subsequential limit set) that lies in .
Compactness is a property of alone. The covering families range over open subsets of , not over sets open in some other ambient space, so the notion defined here is compactness of as a subset of . Nothing below relativises it to a smaller ambient field; where an ordered field other than is meant, as in FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness, the whole vocabulary is set up again there for that field.
is compact and sequentially compact. The empty subfamily covers it, and there is no sequence with all terms in , so both conditions hold vacuously.
Remarks
-
Why "finite" is spelled out by listing. A finite subfamily is described here as one that can be written with , which is exactly the form every proof on this page produces or consumes: the bisection argument of Heine-Borel by bisection: every closed bounded interval is compact produces a one-member list, and the arguments of A compact subset of is closed and bounded consume a list by taking a maximum over it (Every nonempty finite set of reals has a maximum and a minimum). Since contains , the shortest nonempty list is .
-
The two notions are not defined to be equivalent, and their equivalence is a theorem. For subsets of it is A subset of is compact iff it is sequentially compact; both of its implications run through the characterisation of compactness by closed and bounded, and its forward implication additionally uses Bolzano-Weierstrass. Neither implication is formal.
-
Compactness is not inherited by subsets, but by closed subsets. A closed subset of a compact set is compact, which is immediate from A subset of is compact if and only if it is closed and bounded once that is available, whereas shows that an arbitrary subset of a compact set need not be compact.
-
The empty cover. If then no open cover of is empty, so the case distinction in the definition of compactness only ever matters for ; it is written out so that the definition does not quietly assume nonempty.