Lower Closure is Increasing

Theorem

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

Let $x, y$ be elements of $S$ such that

$x \preceq y$

Then:

$x^\preceq \subseteq y^\preceq$

where $y^\preceq$ denotes the lower closure of $y$.

Proof

Let $z \in x^\preceq$.

By definition of lower closure of element:

$z \preceq x$

By definition of transitivity:

$z \preceq y$

Thus again by definition of lower closure of element:

$z \in y^\preceq$

$\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:21