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 be a poset (Partial order and partially ordered set) and .
An element is an upper bound of if for every .
An element is a least upper bound (or supremum) of if is an upper bound of and for every upper bound of . When it exists we write .
An element is a strict upper bound of if for every .
Remarks
- A least upper bound is unique when it exists. If and are both least upper bounds of then each is an upper bound and each is below the other, so and , whence by antisymmetry (Partial order and partially ordered set). This is what makes the notation 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 and to . 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 and has no fixed point.
- Every element of is an upper bound of the empty set, vacuously. Consequently , when it exists, is the least element of .
- An upper bound of need not belong to , and may have many upper bounds and no least one. In with its usual order, the set has upper bounds but no least upper bound.
- In a poset, a strict upper bound is exactly an upper bound outside . If is strict then , since is impossible. Conversely, if is an upper bound and , then every satisfies and , hence . 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
- Orthonormal eigenbasis for a compact self adjoint operator Corollary
- (ℕ, ≤) has no maximal element: Zorn's chain hypothesis fails Counterexample
- A progressive map with no fixed point, on a poset that is not chain-complete Counterexample
- A sequence with limsup = +∞: the greatest subsequential limit exists only in ℝ̄ Counterexample
- xₖ = 1 + (-1)ᵏ, yₖ = 1 + (-1)ᵏ⁺¹ give limsup(xₖ yₖ) = 0 < 4 Counterexample
- Chain-complete poset Definition
- Comparison angles of hinges, model triangle angles, and the Alexandrov upper angle Definition
- Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles Definition
- Real powers from suprema of rational powers, with the reciprocal convention below base one Definition
- Short loops, the uniform-plus-length topology, short-loop homotopies, and nonshrinkability Definition
- The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness Definition
- The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua Definition
- (-1)ᵏ has liminf = -1 and limsup = 1, so it does not converge Example
- A positive sequence making all three inequalities of the ratio-to-root chain strict Example
- Assuming the Axiom of Choice, compactness of [0,1] derived from the subbase lemma alone, using only the rays as a subbasis and the least upper bound property Example
- The block sequence 1/1; 1/2, 2/2; 1/3, 2/3, 3/3; … has subsequential limit set exactly [0,1] Example
- The chains of a poset, ordered by inclusion, form a chain-complete poset Example
- The power set is chain-complete, with union as supremum Example
- FALSE: limsup aₖ^1/k = limsup aₖ₊₁/aₖ for every positive sequence False statement
- FALSE: limsup(xₖ + yₖ) = limsup xₖ + limsup yₖ False statement
- A supremum of extremal elements is extremal Lemma
- An ordered field with the least-upper-bound property has the nested interval property and is Archimedean Lemma
- Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces Lemma
- Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences Lemma
- Every subset of ℝ̄ has a least upper bound and a greatest lower bound in ℝ̄, agreeing with the real supremum and infimum on nonempty sets bounded in ℝ Lemma
- For finite L: L = limsup xₖ iff for every ε > 0 one has xₖ < L + ε eventually and xₖ > L - ε frequently Lemma
- Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas Lemma
- If xₖ ≤ yₖ eventually then limsup xₖ ≤ limsup yₖ and liminf xₖ ≤ liminf yₖ Lemma
- Length in a metric target: lower semicontinuity and arc-length reparametrization Lemma
- liminf xₖ ≤ limsup xₖ for every real sequence Lemma
- limsup(-xₖ) = -liminf(xₖ), with the reflection of ℝ̄ exchanging ±∞ Lemma
- Normal relative property (T) controls the distance to the invariant subspace Lemma
- The cut at an extremal element is closed under chain suprema Lemma
- The monotone convergence property plus the Archimedean property imply the least-upper-bound property Lemma
- The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk Lemma
- The tail suprema of any real sequence are nonincreasing in ℝ̄, so the limit superior exists for every sequence Lemma
- The union of a nonempty chain of filters is a filter Lemma
- A linear continuum is connected in its order topology, and so is every order-convex subset of it Theorem
- A real sequence converges to L ∈ ℝ iff liminf xₖ = limsup xₖ = L, and diverges to ±∞ iff both equal ±∞ Theorem
- A summability matrix with only finitely many nonzero entries per row is regular iff each column tends to 0, the row sums tend to 1, and the row absolute sums are uniformly bounded Theorem
…and 13 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
- Upper and lower bounds (Wikipedia) (standard reference, not scraped)
- Partially ordered set (Wikipedia) (standard reference, not scraped)