Supremum by Suprema of Directed Set in Simple Order Product
Theorem
Let $\struct {S, \preceq}$ be an up-complete meet semilattice.
Let $\struct {S \times S, \precsim}$ be the simple order product of $\struct {S, \preceq}$ and $\struct {S, \preceq}$.
Let $D$ be a directed subset of $S \times S$.
Then:
- $\sup D = \tuple {\map \sup {\map {\pr_1^\to} D}, \map \sup {\map {\pr_2^\to} D} }$
where
- $\pr_1$ denotes the first projection on $S \times S$
- $\pr_2$ denotes the second projection on $S \times S$
- $\map {\pr_1^\to} D$ denotes the image of $D$ under $\pr_1$
Proof
- $\struct {S \times S, \precsim}$ is up-complete.
By definition of up-complete:
- $D$ admits a supremum.
By definition of Cartesian product:
- $\exists d_1, d_2 \in S: \sup D = \tuple {d_1, d_2}$
By Up-Complete Product/Lemma 2:
- $D_1 := \map {\pr_1^\to} D$ is directed
and
- $D_2 := \map {\pr_2^\to} D$ is directed.
By definition of up-complete:
- $D_1$ admits a supremum
and
- $D_2$ admits a supremum
We will prove that
- $d_2$ is upper bound for $D_2$
Let $x \in D_2$.
By definition of image of set:
- $\exists \tuple {a, b} \in D: \map {\pr_2} {a, b} = x$
By definition of second projection: $b = x$
By definition of supremum:
- $\tuple {d_1, d_2}$ is upper bound for $D$.
By definition of upper bound:
- $\tuple {a, x} \precsim \tuple {d_1, d_2}$
Thus by definition of simple order product:
- $x \preceq d_2$
$\Box$
Analogically we have that
- $d_1$ is upper bound for $D_1$
By definition of supremum:
- $\sup D_1 \preceq d_1$ and $\sup D_2 \preceq d_2$
By definition of simple order product:
- $\tuple {\sup D_1, \sup D_2} \precsim \sup D$
By Up-Complete Product/Lemma 1:
- $D_1 \times D_2$ is directed.
By definition of up-complete:
- $D_1 \times D_2$ admits a supremum.
By definition of subset:
- $D \subseteq D_1 \times D_2$
- $\sup D \precsim \map \sup {D_1 \times D_2}$
By Supremum of Simple Order Product:
- $\sup D \precsim \tuple {\sup D_1, \sup D_2}$
Thus by definition of antisymmetry:
- $\sup D = \tuple {\sup D_1, \sup D_2}$
$\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 WAYBEL_2:12