ThmDex – An index of mathematical definitions, results, and conjectures.

Result R1076 on D667: Minimum element

Minimum element is unique

Formulation 0

Let $P = (X, {\preceq})$ be a D1103: Partially ordered set such that

(i)	$X \neq \emptyset$

Let $a, b \in X$ each be a D2218: Set element in $X$ such that

(i)	\begin{equation} \forall \, x \in X : a \preceq x \end{equation}
(ii)	\begin{equation} \forall \, x \in X : b \preceq x \end{equation}

Then \begin{equation} a = b \end{equation}

Proofs

Proof 0

Let $P = (X, {\preceq})$ be a D1103: Partially ordered set such that

(i)	$X \neq \emptyset$

Let $a, b \in X$ each be a D2218: Set element in $X$ such that

(i)	\begin{equation} \forall \, x \in X : a \preceq x \end{equation}
(ii)	\begin{equation} \forall \, x \in X : b \preceq x \end{equation}

This result is an D5370: Order dual theorem to result R1077: Maximum element is unique, whence the claim is a consequence of R1323: Order duality principle. $\square$