Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge 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.

A subset of R is compact if and only if it is closed and bounded

Statement

Let K⊆R. Then K is compact (Open cover, subcover, compact subset of R (every open cover has a finite subcover), and sequentially compact subset) if and only if K is closed (Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen) and bounded (Lower bound, bounded below, bounded set).

This is the Heine-Borel theorem in the form used everywhere below. The forward implication is A compact subset of R is closed and bounded and spends no completeness, only the Archimedean property and the existence of maxima of finite sets; the backward implication rests on Heine-Borel by bisection: every closed bounded interval [a,b] is compact and therefore on the completeness of R, and the remarks below record where it fails without completeness.

Facts & Assumptions

Given: A subset K⊆R.

[L1]

Open cover, finite subfamily and compactness; the empty subfamily covers ∅ (Open cover, subcover, compact subset of R (every open cover has a finite subcover), and sequentially compact subset).

[L2]

A compact subset of R is closed and bounded (A compact subset of R is closed and bounded).

[L3]

Every closed bounded interval [ℓ,u] with ℓ≤u is compact (Heine-Borel by bisection: every closed bounded interval [a,b] is compact).

[L5]

K is bounded exactly when there are ℓ,u∈R with ℓ≤y≤u for every y∈K (Lower bound, bounded below, bounded set).

[L6]

[ℓ,u]={ z∈R:ℓ≤z≤u } (Intervals of R: the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct
1.1

If K is compact then K is closed and bounded, which is [L2]; this is the forward implication.

L2
1.2

For the backward implication assume K is closed and bounded. If K=∅ then every open cover of K admits the empty subfamily as a finite subcover, so K is compact.

assume-hypL1
1.3

Assume moreover K≠∅; fix s∈K and, by [L5], reals ℓ,u with ℓ≤y≤u for every y∈K. Then ℓ≤s≤u, so ℓ≤u, and K⊆[ℓ,u] by [L6].

assume-hypL5L6choose
2.1

Let U be an open cover of K and put W:=U∪{R∖K}. Every member of W is open, since R∖K is open by [L4], and W covers [ℓ,u]: a point of [ℓ,u] either lies in K, hence in some member of U, or lies outside K, hence in R∖K.

step 1.3L1L4
3.1

By [L3] the interval [ℓ,u] is compact, so some finite subfamily {W0,…,Wp} of W covers [ℓ,u], where the case of an empty subfamily is possible only when [ℓ,u]=∅, which is excluded by ℓ≤u. Put V:={ Wi:Wi∈U }, a finite subfamily of U. Then K⊆⋃V: a point y∈K⊆[ℓ,u] lies in some Wi, and Wi cannot be a member of W outside U, because the only such member is R∖K and y∈K; so Wi∈U and Wi∈V.

step 2.1L1L3L6
4.1

Every open cover of a nonempty closed bounded K therefore has a finite subcover, so such a K is compact; together with the empty case of step 1.2 this proves the backward implication, and step 1.1 is the forward one.

step 1.1step 1.2step 3.1L1∎

Remarks

Depends on

Used by

Dependency tree · two levels

26 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