Infimum of Empty Set is Greatest Element

Theorem

Let $\struct {S, \preceq}$ be an ordered set.

Suppose that $\map \inf \O$, the infimum of the empty set, exists in $S$.

Then $\forall s \in S: s \preceq \map \inf \O$.

That is, $\map \inf \O$ is the greatest element of $S$.

Proof

Observe that, vacuously, any $s \in S$ is a lower bound for $\O$.

But for any lower bound $s$ of $\O$, $s \preceq \map \inf \O$ by definition of infimum.

Hence:

$\forall s \in S: s \preceq \map \inf \O$

$\blacksquare$

Also see

• Supremum of Empty Set is Smallest Element