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.

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.1

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.

baseA1L1L3

1.2

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.

ihA1

2.1

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}}$ .

step 1.2L1

3.1

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.

step 2.1L1L3

3.2

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.

step 2.1L1L3

4.1

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)$ .

step 3.1step 3.2A1

5.1

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.

step 1.1step 4.1givenL2discharge-induction∎

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

…and 88 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)