Up-Complete Product/Lemma 1
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq_1}$, $\struct {T, \preceq_2}$ be non-empty ordered sets.
Let $\struct {S \times T, \preceq}$ be the simple order product of $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$.
Let $X$ be a directed subset of $S$.
Let $Y$ be a directed subset of $T$.
Then $X \times Y$ is also a directed subset of $S \times T$.
Proof
Let $\tuple {s_1, t_1}, \tuple {s_2, t_2} \in X \times Y$.
By definition of Cartesian product:
- $s_1, s_2 \in X$ and $t_1, t_2 \in Y$
By definition of directed subset:
- $\exists h_1 \in X: s_1 \preceq_1 h_1 \land s_2 \preceq_1 h_1$
and
- $\exists h_2 \in X: t_1 \preceq_2 h_2 \land t_2 \preceq_2 h_2$
By definition of simple order product:
- $\exists \tuple {h_1, h_2} \in X \times Y: \tuple {s_1, t_1} \preceq \tuple {h_1, h_2} \land \tuple {s_2, t_2} \preceq \tuple {h_1, h_2}$
Thus by definition:
- $X \times Y$ is a directed subset of $S \times T$.
$\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 YELLOW_3:funcreg 9