Upper Closure is Decreasing

Theorem

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

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

$x \preceq y$

then $y^\succeq \subseteq x^\succeq$

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

Proof

Let $z \in y^\succeq$.

By definition of upper closure of element:

$y \preceq z$

By definition of ordering, $\preceq$ is transitive.

From $x \preceq y$ and $y \preceq z$:

$x \preceq z$

Thus again by definition of upper closure of element:

$z \in x^\succeq$

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