Up-Complete Product/Lemma 2
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 \times T$.
Then
- $\map {\pr_1^\to} X$ and $\map {\pr_2^\to} X$ are directed
where
- $\pr_1$ denotes the first projection on $S \times T$
- $\pr_2$ denotes the second projection on $S \times T$
- $\map {\pr_1^\to} X$ denotes the image of $X$ under $\pr_1$
Proof
Let $x, y \in \map {\pr_1^\to} X$.
By definitions of image of set and projections:
- $\exists x' \in T: \tuple {x, x'} \in X$
and
- $\exists y' \in T: \tuple {y, y'} \in X$
By definition of directed:
- $\exists \tuple {a, b} \in X: \tuple {x, x'} \preceq \tuple {a, b} \land \tuple {y, y'} \preceq \tuple {a, b}$
By definition of simple order product:
- $\exists a \in \map {\pr_1^\to} X: x \preceq_1 a \land y \preceq_1 a$
Thus by definition
- $\map {\pr_1^\to} X$ is directed.
By mutatis mutandis:
- $\map {\pr_2^\to} X$ is directed.
$\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:22