DefinitionDefinition: Literature-sourcedProof: Not applicablejudge 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.
Lower bound, bounded below, bounded set
Definition
Throughout, denotes the complete ordered field (Complete ordered field (least-upper-bound property)) and is a subset of it.
The notions upper bound and bounded above are already fixed by Complete ordered field (least-upper-bound property) and are only recalled here, never redefined: is an upper bound of if for all , and is bounded above if it has at least one upper bound. The dual notions are:
- is a lower bound of if for all .
- is bounded below if it has at least one lower bound.
- is bounded if it is both bounded above and bounded below, that is, if there are with for every .
Remarks
- A bound is an element of and is not required to lie in . A bound that does lie in is a maximum or a minimum (Maximum and minimum of a set), and that is a strictly stronger condition (FALSE: the supremum of a set belongs to the set).
- Bounds come in half-lines: if is a lower bound of then so is every , and if is an upper bound then so is every . Consequently a set that has one bound of a given kind has infinitely many, and the interesting question is whether the collection of them has a best element, which is what a supremum (Complete ordered field (least-upper-bound property)) or an infimum (Greatest lower bound (infimum)) is.
- Bounded above and bounded below are independent conditions. The set of canonical naturals of is bounded below by (Canonical naturals are positive and strictly increasing) and is not bounded above (Every complete ordered field is Archimedean); its reflection is bounded above and not bounded below (Reflection through zero exchanges upper and lower bounds).
- The empty set is bounded, and vacuously so: every real number is both an upper bound and a lower bound of , since the defining condition quantifies over no elements. Having bounds is therefore much weaker than having a least upper bound or a greatest lower bound (FALSE: every subset of has a supremum).