Infimum of Upper Closure of Element

Theorem

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

Let $s$ be an element of $S$.

Then:

$\map \inf {s^\succeq} = s$

where $s^\succeq$ denotes the upper closure of $s$.

Proof

\(\ds \map \inf {s^\succeq}\)

\(=\)

\(\ds \map \inf {\set s^\succeq}\)

Upper Closure of Singleton

\(\ds \)

\(=\)

\(\ds \map \inf {\set s}\)

Infimum of Upper Closure of Set

\(\ds \)

\(=\)

\(\ds s\)

Infimum of Singleton

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL_0:39