LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

Every nonempty finite set of reals has a maximum and a minimum

Statement

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

What is proved below is exactly the displayed statement, by induction on $n$ .

The usual reading, that every nonempty finite subset of $R$ has a maximum and a minimum, follows once one identifies the nonempty finite subsets of $R$ with the sets listable as ${a_{0}, \dots, a_{n}}$ . That identification is recorded as a stipulation in the Given below, because this page has no definition of finiteness to prove it against. It is discharged, not merely assumed: The nonempty finite subsets of $R$ are exactly the listable ones proves that the two descriptions of a nonempty finite subset of $R$ agree. That lemma is recorded in justified_by rather than in deps, since it is about the sets this lemma quantifies over and therefore depends on this one. This is what licenses the notation $\max {a_{1}, \dots, a_{n}}$ and $\min {a_{1}, \dots, a_{n}}$ for finite sets of real numbers from this page onwards.

Statement references

Maximum and minimum of a set

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

Facts & Assumptions

Given: Real numbers $a_{0}, a_{1}, a_{2}, \dots$ ; for $n \in N$ write $F_{n} : = {a_{0}, \dots, a_{n}}$ , so that $F_{n + 1} = F_{n} \cup {a_{n + 1}}$ . A subset of $R$ is nonempty and finite exactly when it equals $F_{n}$ for some $n \in N$ and some choice of $a_{0}, \dots, a_{n}$ .

[A1]

$P (n)$ denotes the statement: for all $a_{0}, \dots, a_{n} \in R$ , the set $F_{n}$ has a maximum and a minimum.

[L1]

Maximum and minimum: $m = \max X$ means $m \in X$ and $x \leq m$ for all $x \in X$ ; $m = \min X$ means $m \in X$ and $m \leq x$ for all $x \in X$ ; each is unique when it exists (Maximum and minimum of a set).

[L2]

Induction principle: if $P (0)$ holds and $P (n)$ implies $P (n + 1)$ for every $n \in N$ , then $P (n)$ holds for every $n \in N$ , where $n + 1$ denotes the successor $σ (n)$ (The principle of mathematical induction, Addition of natural numbers).

[L3]

The order on $R$ is reflexive, total and transitive: $a \leq a$ ; for all $a, b$ exactly one of $a < b$ , $a = b$ , $b < a$ holds, so at least one of $a \leq b$ and $b \leq a$ holds; and $a \leq b$ with $b \leq c$ gives $a \leq c$ (Complete ordered field (least-upper-bound property), Ordered field).

Proof

technique · induction

1.1baseA1L1L3

Base case: $F_{0} = {a_{0}}$ , and $a_{0} \in F_{0}$ with $a_{0} \leq a_{0}$ by reflexivity, so $a_{0}$ is both a maximum and a minimum of $F_{0}$ ; hence $P (0)$ holds.

1.2ihA1

Inductive hypothesis: fix $n \in N$ and assume $P (n)$ , that is, for all reals $a_{0}, \dots, a_{n}$ the set $F_{n}$ has a maximum and a minimum.

2.1step 1.2L1

Let $a_{0}, \dots, a_{n + 1} \in R$ be arbitrary; by the inductive hypothesis the set $F_{n}$ has a maximum $M$ and a minimum $m$ , and $F_{n + 1} = F_{n} \cup {a_{n + 1}}$ .

3.1step 2.1L1L3

By totality at least one of $a_{n + 1} \leq M$ and $M \leq a_{n + 1}$ holds. If $a_{n + 1} \leq M$ , then $M \in F_{n} \subseteq F_{n + 1}$ , every element of $F_{n}$ is $\leq M$ because $M = \max F_{n}$ , and $a_{n + 1} \leq M$ as well, so $M$ is a maximum of $F_{n + 1}$ . If $M \leq a_{n + 1}$ , then $a_{n + 1} \in F_{n + 1}$ , every $x \in F_{n}$ satisfies $x \leq M \leq a_{n + 1}$ hence $x \leq a_{n + 1}$ by transitivity, and $a_{n + 1} \leq a_{n + 1}$ , so $a_{n + 1}$ is a maximum of $F_{n + 1}$ . Either way $F_{n + 1}$ has a maximum.

3.2step 2.1L1L3

Dually, at least one of $m \leq a_{n + 1}$ and $a_{n + 1} \leq m$ holds. If $m \leq a_{n + 1}$ , then $m \in F_{n + 1}$ and every element of $F_{n + 1}$ is $\geq m$ , so $m$ is a minimum of $F_{n + 1}$ . If $a_{n + 1} \leq m$ , then $a_{n + 1} \in F_{n + 1}$ and every $x \in F_{n}$ satisfies $a_{n + 1} \leq m \leq x$ hence $a_{n + 1} \leq x$ by transitivity, so $a_{n + 1}$ is a minimum of $F_{n + 1}$ . Either way $F_{n + 1}$ has a minimum.

4.1step 3.1step 3.2A1

Since $a_{0}, \dots, a_{n + 1}$ were arbitrary, $F_{n + 1}$ has a maximum and a minimum for every such list, that is, $P (n)$ implies $P (n + 1)$ .

5.1step 1.1step 4.1givenL2discharge-induction∎

The base case and the inductive step give $P (n)$ for every $n \in N$ by the induction principle; since a nonempty finite subset of $R$ is exactly a set of the form $F_{n}$ , every nonempty finite subset of $R$ has both a maximum and a minimum.

Remarks

Where the stipulation is discharged. Finiteness itself is defined later, in Finite, countably infinite, countable, uncountable, as equinumerosity with a von Neumann natural; with that definition in hand The nonempty finite subsets of $R$ are exactly the listable ones proves that a subset of $R$ is nonempty and finite exactly when it is listable as ${a_{0}, \dots, a_{n}}$ , which is the Given below. So nothing on this page rests on an assumption that is never paid for; it is paid for later, and the payment is recorded in justified_by.
Only the total order is used, never completeness. The base case needs reflexivity, the inductive step needs totality and transitivity, and the induction itself runs over $N$ . The same induction works in any totally ordered field; what is recorded here is its specialisation to $R$ .
Nonemptiness is essential: $\emptyset$ is finite and has no maximum (Maximum and minimum of a set). Finiteness is essential too: ${x \in R : 0 < x < 1}$ is bounded and has no maximum (FALSE: the supremum of a set belongs to the set).
Combined with claim 1 of The supremum is attained exactly when a maximum exists, this says every nonempty finite subset of $R$ has a supremum, and that the supremum is attained, because it equals the maximum. The infimum half is not part of The supremum is attained exactly when a maximum exists, which speaks only of maxima and suprema; it follows from the minimum proved here together with the reflection identity $\inf X = - \sup (- X)$ (Reflection through zero exchanges upper and lower bounds, Every nonempty set bounded below has an infimum).

Depends on

Used by

Bias-corrected AMSGrad update Algorithm
CFL-monotone upwind update for first-order HJB equations Algorithm
Explicit monotone diagonal-diffusion Bellman grid update Algorithm
Finite-budget adaptive Runge–Kutta controller Algorithm
Finite-budget deterministic direct search with positive-spanning polling Algorithm
Finite-budget Howard policy iteration for a discounted generator Bellman system Algorithm
Finite-budget Nelder–Mead simplex procedure Algorithm
Finite-horizon model-predictive control Algorithm
Finite-memory-free proximal bundle method with serious and null steps Algorithm
Positive-interpolation semi-Lagrangian update for first-order HJB equations Algorithm
Projected subgradient method with finite budget Algorithm
Trial-based real-time dynamic programming Algorithm
Uncorrected Adam for online convex losses Algorithm
Uncorrected AMSGrad with a coordinatewise historical maximum Algorithm
A connected graph with pairwise distinct edge weights has a unique minimum spanning tree Corollary
A continuous real function on a compact subset of ℝ is bounded Corollary
[0,1) is neither open nor closed in ℝ Counterexample
A function differentiable on [0,1] whose derivative is unbounded, hence not Riemann integrable Counterexample
Cyclic exact block minimization can cycle outside the convex separable hypotheses Counterexample
ℕ with the discrete metric is bounded and is not totally bounded Counterexample
On (0,∞) the metrics |x-y| and |1/x - 1/y| have the same topology and are not uniformly equivalent Counterexample
On (0,∞) the metrics |x-y| and |1/x - 1/y| share their topology and not their Cauchy sequences Counterexample
On ℝ the metrics |x-y| and min(|x-y|,1) are uniformly but not Lipschitz equivalent Counterexample
Refuted: a pointwise bounded family of continuous functions is equicontinuous. The spikes are bounded by 1 everywhere and are not equicontinuous at 0 Counterexample
Refuted: C(X,Y) is closed in the topology of pointwise convergence. The ramps on [0,1] converge pointwise to a discontinuous limit Counterexample
Refuted: convergence uniformly on every compact subset of ℝ implies uniform convergence. The maps x ↦ x/(n+1) separate the two Counterexample
The cover {(1/k, 1)} of (0,1) has no finite subcover, so (0,1) is not compact Counterexample
The identity on (0,1) is bounded with no greatest value, and on [0,∞) it is continuous and unbounded Counterexample
The open interval (0,1) is totally bounded and not compact, the cover by the intervals (1/(k+2), 1) having no finite subcover Counterexample
x ↦ 1/x is continuous on (0,1) and sends the Cauchy sequence (1/(k+2))_k ≥ 0 to an unbounded one Counterexample
ℤ and {n + 1/n : n ≥ 2} are disjoint closed subsets of ℝ at distance 0, so the set-to-set distance is not a metric Counterexample
ℤ is closed and not compact, and (0,1) is bounded and not compact: neither hypothesis of Heine-Borel can be dropped Counterexample
Acceptance polynomials and approximate degree on Boolean domains Definition
Bellman optimality operator Definition
Best s-term ℓ1 approximation error Definition
Circular phase distance modulo one Definition
Finite learned transition and reward models Definition
Finite Markov decision process with joint reward-transition law Definition
Finite-state discounted generator Bellman system Definition
Grid partitions of a rectangle in ℝᵐ, their cells, refinements and mesh Definition

…and 159 more results.

Dependency tree · two levels

11 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

Maximum and minimum (Wikipedia) (standard reference, not scraped)
Mathematical induction (Wikipedia) (standard reference, not scraped)
Finite set (Wikipedia) (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)