Compact Closure is Increasing

Theorem

Let $\left({S, \preceq}\right)$ be an ordered set.

Let $x, y \in S$ such that

$x \preceq y$

Then $x^{\mathrm{compact} } \subseteq y^{\mathrm{compact} }$

where $x^{\mathrm{compact} }$ denotes the compact closure of $x$.

Proof

Let $z \in x^{\mathrm{compact} }$

By definition of compact closure:

$z$ is a compact element and $z \preceq x$

By definition of transitivity:

$z \preceq y$

Thus by definition of compact closure:

$z \in y^{\mathrm{compact} }$

$\blacksquare$

Sources

• Mizar article WAYBEL13:1