ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Binary endorelation ▼ Preordering relation ▼ Partial ordering relation ▼ Partially ordered set ▼ Minimal element ▼ Minimum element ▼ Set lower bound ▼ Set of lower bounds
Definition D301
Infimum element

Let $P = (X, {\preceq})$ be a D1103: Partially ordered set.
Let $\mathsf{LB} = \mathsf{LB}_P(E)$ be the D553: Set of lower bounds of $E \subseteq X$ with respect to $P$.
A D2218: Set element $x_0 \in X$ is an infimum of $E$ with respect to $P$ if and only if
 (1) $x_0 \in \mathsf{LB}$ (2) $\forall \, x \in \mathsf{LB} : x \preceq x_0$

Let $P = (X, {\preceq})$ be a D1103: Partially ordered set.
Let $\mathsf{LB} = \mathsf{LB}_P(E)$ be the D553: Set of lower bounds of $E \subseteq X$ with respect to $P$.
A D2218: Set element $x_0 \in X$ is an infimum of $E$ with respect to $P$ if and only if
 (1) $x_0 \in \mathsf{LB}$ (2) $\forall \, x \in \mathsf{LB} : (x, x_0) \in {\preceq}$