Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26
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 R (every open cover has a finite subcover), and sequentially compact subset

Definition

Let K⊆R, with open sets as in Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen.

  • An open cover of K is a family U of open subsets of R with K⊆⋃U.
  • A subcover of U is a subfamily V⊆U that is still an open cover of K.
  • A subfamily V⊆U is finite when V=∅ or there are n∈N and members U0,…,Un of U with V={U0,…,Un}; repetitions in the list are allowed and harmless.
  • K is compact when every open cover of K has a finite subcover: for every open cover U of K, either K=∅ and the empty subfamily covers it, or there are n∈N and U0,…,Un∈U with K⊆U0∪⋯∪Un.
  • K is sequentially compact when every sequence (xk) of reals with xk∈K for all k∈N (Sequences of reals: bounded, eventually, frequently, tails, subsequences) has a subsequence converging (Limits and Cauchy sequences of reals) to some point of K; equivalently, when every such sequence has a subsequential limit (Subsequential limit of a real sequence, and the subsequential limit set) that lies in K.

Compactness is a property of K alone. The covering families range over open subsets of R, not over sets open in some other ambient space, so the notion defined here is compactness of K as a subset of R. Nothing below relativises it to a smaller ambient field; where an ordered field other than R 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 {U0,…,Un} with n∈N, 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 [a,b] is compact produces a one-member list, and the arguments of A compact subset of R 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 N contains 0, the shortest nonempty list is {U0}.

  • The two notions are not defined to be equivalent, and their equivalence is a theorem. For subsets of R it is A subset of R 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 R is compact if and only if it is closed and bounded once that is available, whereas (0,1)⊆[0,1] shows that an arbitrary subset of a compact set need not be compact.

  • The empty cover. If K≠∅ then no open cover of K is empty, so the case distinction in the definition of compactness only ever matters for K=∅; it is written out so that the definition does not quietly assume K nonempty.

Depends on

Used by

Dependency tree · two levels

16 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