Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $a$ be a set, $\le$ a partial order on $a$, and $s$ a subset of $a$.

¶ An element $b\in a$ is an upper bound of $s$ if $v\le b$ for every $v\in s$, and a lower bound of $s$ if $b\le v$ for every $v\in s$. The classes of upper bounds and of lower bounds of $s$ in $a$ are

$$\operatorname{Ub}(s)=\{b\in a:\forall v\,(v\in s\Rightarrow v\le b)\},\qquad\operatorname{Lb}(s)=\{b\in a:\forall v\,(v\in s\Rightarrow b\le v)\},$$

formed by restricted class abstraction with the parameters $s$ and $\le$; their formulas quantify over set variables only, the ordered pair being a defined set symbol, so they are predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. Both are subclasses of $a$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted, hence subsets of $a$ by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass.

¶ $s$ is bounded above if it has an upper bound, bounded below if it has a lower bound, and bounded if it is both bounded above and bounded below.

¶ An element $m$ is a least element of $s$ if $m\in s$ and $m\le v$ for every $v\in s$, and a greatest element of $s$ if $m\in s$ and $v\le m$ for every $v\in s$. By Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §least-unique, $s$ has at most one least element and at most one greatest element; when it has a least element, $\min s$ denotes it: the unique set $z$ satisfying the predicative formula $z\in s\wedge\forall v\,(v\in s\Rightarrow z\le v)$. When it has a greatest element, $\max s$ denotes it: the unique set $z$ satisfying $z\in s\wedge\forall v\,(v\in s\Rightarrow v\le z)$. Thus $\min s$ and $\max s$ are defined set symbols, used only when the least element, respectively the greatest element, exists.

¶ A supremum (or least upper bound) of $s$ is a least element of $\operatorname{Ub}(s)$, and an infimum (or greatest lower bound) of $s$ is a greatest element of $\operatorname{Lb}(s)$. By Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §least-unique, applied to the subsets $\operatorname{Ub}(s)$ and $\operatorname{Lb}(s)$ of $a$, $s$ has at most one supremum and at most one infimum. When $s$ has a supremum, $\sup s$ denotes it: the unique set $z$ satisfying the predicative formula $z\in\operatorname{Ub}(s)\wedge\forall b\,(b\in\operatorname{Ub}(s)\Rightarrow z\le b)$. When $s$ has an infimum, $\inf s$ denotes it: the unique set $z$ satisfying $z\in\operatorname{Lb}(s)\wedge\forall b\,(b\in\operatorname{Lb}(s)\Rightarrow b\le z)$. Thus $\sup s$ and $\inf s$ are defined set symbols, used only when the supremum, respectively the infimum, exists.