LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

The nonempty finite subsets of $R$ are exactly the listable ones

Statement

Let $R$ be a complete ordered field (Complete ordered field (least-upper-bound property)) and let $F \subseteq R$ be nonempty. Then $F$ is finite (Finite, countably infinite, countable, uncountable) if and only if there are $n \in N$ and $a_{0}, a_{1}, \dots, a_{n} \in R$ with

$F = {a_{0}, a_{1}, \dots, a_{n}} .$

Here ${a_{0}, \dots, a_{n}}$ means the image $a [σ (n)]$ of a function $a : σ (n) \to R$ , where $σ (n) = {i \in N : i \leq n}$ (The natural numbers $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ ).

Consequently every nonempty finite subset of $R$ has a maximum and a minimum (Maximum and minimum of a set), since Every nonempty finite set of reals has a maximum and a minimum proves exactly that for sets presented as ${a_{0}, \dots, a_{n}}$ .

Facts & Assumptions

Given: A complete ordered field $R$ and a nonempty subset $F \subseteq R$ . For $n \in N$ and a function $a : σ (n) \to R$ , write ${a_{0}, \dots, a_{n}} : = a [σ (n)]$ , and call a set of this form listable.

[L1]

$F$ is finite when $F \approx m$ for some $m \in N$ , where $m = {i \in N : i < m}$ ; and $F \approx 0 = \emptyset$ only for $F = \emptyset$ (Finite, countably infinite, countable, uncountable, The natural numbers $N$ (von Neumann)).

[L2]

Bijections and their images, and the symmetry and transitivity of $\approx$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection).

[L3]

Induction principle: if $P (0)$ holds and $P (n)$ implies $P (σ (n))$ for every $n$ , then $P (n)$ holds for every $n \in N$ (The principle of mathematical induction).

[L4]

For the additive order of Order on the natural numbers: $i < σ (n) ⟺ i \leq n$ , and every natural number is exactly the set of the naturals below it, so $σ (n) = {i : i \leq n} = n \cup {n}$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , The natural numbers $N$ (von Neumann)); and every nonzero natural is a successor (Every nonzero natural number is a successor).

[L5]

For every $n \in N$ and all $a_{0}, \dots, a_{n} \in R$ the set ${a_{0}, \dots, a_{n}}$ has a maximum and a minimum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L6]

Membership is irreflexive on $N$ : $k \notin k$ for every $k \in N$ (Every natural number is a transitive set and is not a member of itself).

Proof

technique · induction

1.1

Base case of the listable-implies-finite direction: for $n = 0$ a listable set is $a [σ (0)] = {a (0)}$ , and $i \mapsto a (0)$ is a bijection from $σ (0) = {0}$ onto it, so it is finite.

baseL1L2L4

1.2

Inductive hypothesis: fix $n \in N$ and assume every set of the form $a [σ (n)]$ , for a function $a : σ (n) \to R$ , is finite.

1.3

The finite-implies-listable direction needs no induction: if $F$ is nonempty and finite there is a bijection $ψ : m \to F$ with $m \in N$ , and $m \neq 0$ because $F \neq \emptyset$ , so $m = σ (n)$ for some $n$ by [L4]; putting $a : = ψ$ gives $F = ψ [σ (n)] = {a_{0}, \dots, a_{n}}$ , a listable set.

givenL1L2L4

2.1

Inductive step: let $b : σ (σ (n)) \to R$ and put $G = b [σ (n)]$ and $H = b [σ (σ (n))] = G \cup {b (σ (n))}$ , using [L4]. By the inductive hypothesis applied to the restriction of $b$ to $σ (n)$ , there is a bijection $u : G \to k$ for some $k \in N$ . If $b (σ (n)) \in G$ then $H = G$ is finite. Otherwise extend $u$ to $H$ by $u (b (σ (n))) : = k$ ; since $k \notin k$ by [L6], this is a bijection $H \to k \cup {k} = σ (k)$ , so $H$ is finite. In both cases $H$ is finite, so the claim holds at $σ (n)$ .

step 1.2L1L2L4L6

3.1

By [L3] every listable subset of $R$ is finite, and by step 1.3 every nonempty finite subset of $R$ is listable, which is the stated equivalence; combining it with [L5], every nonempty finite $F \subseteq R$ is of the form ${a_{0}, \dots, a_{n}}$ and therefore has a maximum and a minimum.

step 1.1step 1.3step 2.1L3L5discharge-induction∎

Remarks

This lemma discharges the one stipulation left open in Every nonempty finite set of reals has a maximum and a minimum. That lemma proves, by induction on $n$ , that every set ${a_{0}, \dots, a_{n}}$ of reals has a maximum and a minimum, and then adopts as a working convention, explicitly not proved there, that the nonempty finite subsets of $R$ are exactly the sets of that form. The convention could not be proved at the time because the library had no definition of finiteness. With Finite, countably infinite, countable, uncountable available, it is proved above, and the usual reading of that lemma, "every nonempty finite subset of $R$ has a maximum and a minimum", is now a theorem rather than a stipulation.
Nonemptiness is needed only for the finite-implies-listable direction: a list $a_{0}, \dots, a_{n}$ always has at least the entry $a_{0}$ , whereas $\emptyset$ is finite and not listable in this sense.
Nothing in the argument uses the order or the arithmetic of $R$ ; the same proof shows that in any set the nonempty finite subsets are exactly the images of the naturals $σ (n)$ . Only the consequence about maxima and minima uses that $R$ is ordered.

Depends on

Used by

Steinitz's polygonal confinement theorem: finitely many vectors of norm at most 1 summing to 0 can be ordered so that every partial sum has norm at most n Theorem

Cited to discharge well-definedness by Every nonempty finite set of reals has a maximum and a minimum.

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

J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
J. Lebl, Basic Analysis: Introduction to Real Analysis, basic set theory (standard reference, not scraped)
Finite set (Wikipedia) (standard reference, not scraped)
Maximum and minimum (Wikipedia) (standard reference, not scraped)

The nonempty finite subsets of RR are exactly the listable ones