LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (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.

The cut at an extremal element is closed under chain suprema

Statement

Let $(P, \leq)$ be a chain-complete poset, $f : P \to P$ progressive, $M$ the smallest admissible set, and $x \in M$ extremal (Extremal element and its cut (Bourbaki–Witt)). Then $\sup C \in M_{x}$ for every chain $C \subseteq M_{x}$ .

Facts & Assumptions

Given: A chain-complete poset $(P, \leq)$ , a progressive $f : P \to P$ , the smallest admissible set $M$ , an extremal $x \in M$ , and a chain $C \subseteq M_{x}$ .

[A1]

$M_{x} = {z \in M : z \leq x or f (x) \leq z}$ (Extremal element and its cut (Bourbaki–Witt)).

[L1]

$M$ is admissible, so it is closed under $f$ and under suprema of its chains (A smallest admissible set exists).

[L2]

Every chain of $P$ has a least upper bound in $P$ (Chain-complete poset).

[L3]

A least upper bound of a set is itself an upper bound of that set and is below every other upper bound (Upper bound, least upper bound, and strict upper bound).

[L4]

$\leq$ is a partial order, in particular transitive: $u \leq v$ and $v \leq w$ imply $u \leq w$ (Partial order and partially ordered set).

Proof

technique · cases

1.1

Write $s = \sup C$ , which exists in $P$ because $C$ is a chain.

L2construct

1.2

Since $C \subseteq M_{x} \subseteq M$ and $M$ is closed under suprema of its chains, $s \in M$ .

A1L1

1.3

Suppose every $z \in C$ satisfies $z \leq x$ .

assume-case under

1.4

Suppose some $z_{0} \in C$ satisfies $z_{0} \leq̸ x$ .

assume-case over

2.1

In the first case $x$ is an upper bound of $C$ , so $s \leq x$ because $s$ is the least upper bound, hence $s \in M_{x}$ .

step 1.3step 1.1L3step 1.2A1

2.2

In the second case $z_{0} \in M_{x}$ together with $z_{0} \leq̸ x$ forces $f (x) \leq z_{0}$ , and $z_{0} \leq s$ since $s$ is an upper bound of $C$ , so $f (x) \leq s$ by transitivity, hence $s \in M_{x}$ .

step 1.4A1step 1.1step 1.2L3L4

3.1

Either every element of $C$ is below $x$ or some element is not, so the two cases are exhaustive and $\sup C \in M_{x}$ in both.

step 2.1step 2.2cases-exhaustive∎

Remarks

The empty chain is covered without a separate argument: it falls into the first case vacuously, and $\sup \emptyset = ⊥ \leq x$ .
Note which property of the supremum each case uses. The first case uses leastness, that $s$ is below any upper bound; the second uses only that $s$ is an upper bound. Both halves of the definition of least upper bound are needed, which is why chain-completeness cannot be weakened here to the mere existence of some upper bound.
Together with The cut at an extremal element is closed under $f$ this makes $M_{x}$ admissible, which is what Everything in $M$ is comparable to an extremal element feeds to minimality.

Depends on

Used by

Everything in M is comparable to an extremal element Lemma

Dependency tree · two levels

7 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

Mathlib, Order.BourbakiWitt (standard reference, not scraped)
Bourbaki-Witt Principle (Menemui Matematik 39(1), 2017) (standard reference, not scraped)
Bourbaki–Witt theorem (Wikipedia) (standard reference, not scraped)