Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableverified 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.

Upper bound, least upper bound, and strict upper bound

Definition

Let (P,≤) be a poset (Partial order and partially ordered set) and S⊆P.

An element u∈P is an upper bound of S if s≤u for every s∈S.

An element u∈P is a least upper bound (or supremum) of S if u is an upper bound of S and u≤v for every upper bound v of S. When it exists we write u=sup⁡S.

An element u∈P is a strict upper bound of S if s<u for every s∈S.

Remarks

  • A least upper bound is unique when it exists. If u and u′ are both least upper bounds of S then each is an upper bound and each is below the other, so u≤u′ and u′≤u, whence u=u′ by antisymmetry (Partial order and partially ordered set). This is what makes the notation sup⁡S legitimate. Antisymmetry is not peculiar to this argument: the same two-inequality step gives uniqueness of a greatest element (Maximal element and greatest element), and it is used essentially in Bourbaki–Witt fixed point theorem, whose fixed point is obtained by passing from f(c)≤c and c≤f(c) to f(c)=c. Drop antisymmetry and it is the conclusion, not merely the notation, that goes: on two distinct elements each below the other, every subset still has a least upper bound, yet the map exchanging the two satisfies x≤f(x) and has no fixed point.
  • Every element of P is an upper bound of the empty set, vacuously. Consequently sup⁡∅, when it exists, is the least element of P.
  • An upper bound of S need not belong to S, and S may have many upper bounds and no least one. In Q with its usual order, the set {q∈Q:q2<2} has upper bounds but no least upper bound.
  • In a poset, a strict upper bound is exactly an upper bound outside S. If u is strict then u∉S, since u<u is impossible. Conversely, if u is an upper bound and u∉S, then every s∈S satisfies s≤u and s≠u, hence s<u. This distinction from an arbitrary upper bound matters in Zorn's lemma, where the argument must produce one outside the chain.

Depends on

Used by

…and 2 more results.

Dependency tree · one level

1 result within one dependency step 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