Upper Closure of Coarser Subset is Subset of Upper Closure
Jump to navigation
Jump to search
Theorem
Let $L = \left({S, \preceq}\right)$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
- $A$ is coarser than $B$.
Then $A^\succeq \subseteq B^\succeq$
Proof
Let $x \in A^\succeq$
By definition of upper closure of subset:
- $\exists y \in A: y \preceq x$
By definition of coarser subset:
- $\exists z \in B: z \preceq y$
By definition of transitivity:
- $z \preceq x$
Thus by definition of upper closure of subset:
- $x \in B^\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 WAYBEL11:4