Upper Closure of Subset is Subset of Upper Closure
Jump to navigation
Jump to search
Theorem
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $X, Y$ be subsets of $S$.
Then
- $X \subseteq Y \implies X^\succeq \subseteq Y^\succeq$
where $X^\succeq$ denotes the upper closure of $X$.
Proof
Let $X \subseteq Y$.
Let $x \in X^\succeq$.
By definition of upper closure of subset:
- $\exists y \in X: y \preceq x$
By definition of subset:
- $y \in Y$
Thus by definition of upper closure of subset:
- $x \in Y^\succeq$
$\blacksquare$
Sources
- Mizar article YELLOW_3:7