Alphabeta Math
LemmaStatement: 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 compact subset of R is closed and bounded

Statement

Let K⊆R be compact (Open cover, subcover, compact subset of R (every open cover has a finite subcover), and sequentially compact subset). Then 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).

Two covers do the work, and they use the Archimedean property in its two different forms. Boundedness is read off the cover of R by the intervals (−n,n), which needs the cofinal form, that the canonical naturals exceed every real (Every complete ordered field is Archimedean). Closedness is read off the cover of K, for a point x outside it, by the sets { y:∣y−x∣>1/n }, which needs the reciprocal form, that the reciprocals of the naturals get below every positive real (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε); the cofinal form alone does not deliver it.

Facts & Assumptions

Given: A compact set K⊆R. Throughout, n denotes both a natural number ≥1 and the canonical natural n⋅1R of R, as is standard.

[L1]

Open cover, finite subfamily and compactness: every open cover of K has a subcover that is empty or of the form {U0,…,Up} with p∈N (Open cover, subcover, compact subset of R (every open cover has a finite subcover), and sequentially compact subset).

[L2]

U is open when every x∈U admits ε>0 with Nε(x)⊆U; K is closed when R∖K is open; each of the forms (a,b), (a,∞), (−∞,b), R is an open set (Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Intervals of R: the nine order-convex forms, nondegeneracy, and length).

[L3]

Nε(x)={ y:∣y−x∣<ε } (The ε-neighbourhood and the punctured ε-neighbourhood of a point of R).

[L4]

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

[L5]

Archimedean property, cofinal form: for every z∈R there is a natural n≥1 with z<n (Every complete ordered field is Archimedean).

[L6]

Archimedean property, reciprocal form: for every real ε>0 there is a natural n≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean).

[L7]

Absolute value: ∣z∣≥0, ∣z∣≥z, ∣z∣≥−z, and ∣z∣=0 exactly when z=0 (Basic properties of the absolute value).

[L8]

Triangle inequality: ∣p+q∣≤∣p∣+∣q∣ (The triangle inequality).

[L9]

Every nonempty finite set of reals has a maximum, which is one of its members (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L10]

Canonical naturals: n⋅1R>0 for n≥1 and m≤n in N gives m⋅1R≤n⋅1R (Canonical naturals are positive and strictly increasing); reciprocation of positives reverses the order (Inverses of positives are positive, and reciprocation reverses order); the order is total and transitive (Complete ordered field (least-upper-bound property), Ordered field). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Proof

technique · direct
1.1

For each natural n≥1 put Wn:=(−n,n), an open set by [L2]. The family { Wn:n≥1 } covers R, hence covers K: given y∈R, [L5] supplies n≥1 with ∣y∣<n, and then y≤∣y∣<n and −y≤∣y∣<n by [L7], so −n<y<n.

L2L5L7
1.2

Let x∈R∖K and for each natural n≥1 put Vn:={ y∈R:∣y−x∣>1/n }, which is defined because n>0 has a positive inverse by [L10]. Each Vn is open: given y∈Vn, put δ:=∣y−x∣−1/n>0; for z∈Nδ(y) the triangle inequality [L8] gives ∣y−x∣=∣(y−z)+(z−x)∣≤∣y−z∣+∣z−x∣<δ+∣z−x∣, whence ∣z−x∣>∣y−x∣−δ=1/n and z∈Vn. The family { Vn:n≥1 } covers K: for y∈K one has y≠x, so ∣y−x∣>0 by [L7], and [L6] supplies n≥1 with 1/n<∣y−x∣, that is y∈Vn.

L3L6L7L8L10
2.1

Apply compactness to the cover of step 1.1. If the finite subcover is empty then K=∅ and −1≤y≤1 holds vacuously for y∈K; otherwise there are naturals n0,…,np≥1 with K⊆Wn0∪⋯∪Wnp, and putting N:=max⁡{n0,…,np} by [L9] we get Wni⊆WN for each i, since ni≤N gives −N≤−ni and ni≤N in R by [L10]. Hence K⊆WN=(−N,N) and −N≤y≤N for every y∈K, so K is bounded.

step 1.1L1L2L4L9L10
2.2

Apply compactness to the cover of step 1.2. If the finite subcover is empty then K=∅ and ∣y−x∣>1 holds vacuously for y∈K, so take M:=1; otherwise there are naturals n0,…,np≥1 with K⊆Vn0∪⋯∪Vnp, and putting M:=max⁡{n0,…,np} by [L9] we get Vni⊆VM for each i, since ni≤M gives 0<1/M≤1/ni by [L10]. In both cases K⊆VM, that is, ∣y−x∣>1/M for every y∈K.

step 1.2L1L9L10
3.1

Consequently N1/M(x)∩K=∅, since y∈K has ∣y−x∣>1/M while y∈N1/M(x) would give ∣y−x∣<1/M, which trichotomy forbids; so N1/M(x)⊆R∖K. As x was an arbitrary point of R∖K, that complement is open and K is closed.

step 2.2L2L3L10
4.1

K is bounded by step 2.1 and closed by step 3.1, which is the assertion.

step 2.1step 3.1∎

Remarks

Depends on

Used by

Dependency tree · two levels

27 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