Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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\mathbb{R} is closed and bounded

Statement

Let KRK \subseteq \mathbb{R} be compact (Open cover, subcover, compact subset of R\mathbb{R} (every open cover has a finite subcover), and sequentially compact subset). Then KK is closed (Open subset of R\mathbb{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\mathbb{R} by the intervals (n,n)(-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 KK, for a point xx outside it, by the sets {y:yx>1/n}\{\, y : |y - x| > 1/n \,\}, which needs the reciprocal form, that the reciprocals of the naturals get below every positive real (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon); the cofinal form alone does not deliver it.

Facts & Assumptions

Given: A compact set KRK \subseteq \mathbb{R}. Throughout, nn denotes both a natural number 1\ge 1 and the canonical natural n1Rn \cdot 1_{\mathbb{R}} of R\mathbb{R}, as is standard.

[L1]

Open cover, finite subfamily and compactness: every open cover of KK has a subcover that is empty or of the form {U0,,Up}\{U_0, \dots, U_p\} with pNp \in \mathbb{N} (Open cover, subcover, compact subset of R\mathbb{R} (every open cover has a finite subcover), and sequentially compact subset).

[L2]

UU is open when every xUx \in U admits ε>0\varepsilon > 0 with Nε(x)UN_\varepsilon(x) \subseteq U; KK is closed when RK\mathbb{R} \setminus K is open; each of the forms (a,b)(a,b), (a,)(a,\infty), (,b)(-\infty,b), R\mathbb{R} is an open set (Open subset of R\mathbb{R} (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

[L3]

Nε(x)={y:yx<ε}N_\varepsilon(x) = \{\, y : |y - x| < \varepsilon \,\} (The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L4]

KK is bounded when there are ,u\ell, u with yu\ell \le y \le u for every yKy \in K (Lower bound, bounded below, bounded set).

[L5]

Archimedean property, cofinal form: for every zRz \in \mathbb{R} there is a natural n1n \ge 1 with z<nz < n (Every complete ordered field is Archimedean).

[L6]

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

[L7]

Absolute value: z0|z| \ge 0, zz|z| \ge z, zz|z| \ge -z, and z=0|z| = 0 exactly when z=0z = 0 (Basic properties of the absolute value).

[L8]

Triangle inequality: p+qp+q|p + q| \le |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: n1R>0n \cdot 1_{\mathbb{R}} > 0 for n1n \ge 1 and mnm \le n in N\mathbb{N} gives m1Rn1Rm \cdot 1_{\mathbb{R}} \le n \cdot 1_{\mathbb{R}} (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 n1n \ge 1 put Wn:=(n,n)W_n := (-n, n), an open set by [L2]. The family {Wn:n1}\{\, W_n : n \ge 1 \,\} covers R\mathbb{R}, hence covers KK: given yRy \in \mathbb{R}, [L5] supplies n1n \ge 1 with y<n|y| < n, and then yy<ny \le |y| < n and yy<n-y \le |y| < n by [L7], so n<y<n-n < y < n.

L2L5L7
1.2

Let xRKx \in \mathbb{R} \setminus K and for each natural n1n \ge 1 put Vn:={yR:yx>1/n}V_n := \{\, y \in \mathbb{R} : |y - x| > 1/n \,\}, which is defined because n>0n > 0 has a positive inverse by [L10]. Each VnV_n is open: given yVny \in V_n, put δ:=yx1/n>0\delta := |y - x| - 1/n > 0; for zNδ(y)z \in N_\delta(y) the triangle inequality [L8] gives yx=(yz)+(zx)yz+zx<δ+zx|y - x| = |(y - z) + (z - x)| \le |y - z| + |z - x| < \delta + |z - x|, whence zx>yxδ=1/n|z - x| > |y - x| - \delta = 1/n and zVnz \in V_n. The family {Vn:n1}\{\, V_n : n \ge 1 \,\} covers KK: for yKy \in K one has yxy \ne x, so yx>0|y - x| > 0 by [L7], and [L6] supplies n1n \ge 1 with 1/n<yx1/n < |y - x|, that is yVny \in V_n.

L3L6L7L8L10
2.1

Apply compactness to the cover of step 1.1. If the finite subcover is empty then K=K = \varnothing and 1y1-1 \le y \le 1 holds vacuously for yKy \in K; otherwise there are naturals n0,,np1n_0, \dots, n_p \ge 1 with KWn0WnpK \subseteq W_{n_0} \cup \dots \cup W_{n_p}, and putting N:=max{n0,,np}N := \max\{n_0, \dots, n_p\} by [L9] we get WniWNW_{n_i} \subseteq W_N for each ii, since niNn_i \le N gives Nni-N \le -n_i and niNn_i \le N in R\mathbb{R} by [L10]. Hence KWN=(N,N)K \subseteq W_N = (-N,N) and NyN-N \le y \le N for every yKy \in K, so KK is bounded.

step 1.1L1L2L4L9L10
2.2

Apply compactness to the cover of step 1.2. If the finite subcover is empty then K=K = \varnothing and yx>1|y - x| > 1 holds vacuously for yKy \in K, so take M:=1M := 1; otherwise there are naturals n0,,np1n_0, \dots, n_p \ge 1 with KVn0VnpK \subseteq V_{n_0} \cup \dots \cup V_{n_p}, and putting M:=max{n0,,np}M := \max\{n_0, \dots, n_p\} by [L9] we get VniVMV_{n_i} \subseteq V_M for each ii, since niMn_i \le M gives 0<1/M1/ni0 < 1/M \le 1/n_i by [L10]. In both cases KVMK \subseteq V_M, that is, yx>1/M|y - x| > 1/M for every yKy \in K.

step 1.2L1L9L10
3.1

Consequently N1/M(x)K=N_{1/M}(x) \cap K = \varnothing, since yKy \in K has yx>1/M|y - x| > 1/M while yN1/M(x)y \in N_{1/M}(x) would give yx<1/M|y - x| < 1/M, which trichotomy forbids; so N1/M(x)RKN_{1/M}(x) \subseteq \mathbb{R} \setminus K. As xx was an arbitrary point of RK\mathbb{R} \setminus K, that complement is open and KK is closed.

step 2.2L2L3L10
4.1

KK 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources