Up-Complete Product

== 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}$.
Then:
:$\struct {S \times T, \preceq}$ is up-complete both $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ are also up-complete.
== Proof ==
=== Lemma 1 ===
=== Lemma 2 ===
=== Sufficient Condition ===
Assume that:
:$\struct {S \times T, \preceq}$ is up-complete.
Let $X$ be a directed subset of $S$.
By assumption:
:$T \ne \O$
By definition by non-empty set:
:$\exists t: t \in T$
By Singleton is Directed and Filtered Subset:
:$\set t$ is directed
By Lemma 1:
:$X \times \set t$ is a directed subset of $S \times T$
By definition of up-complete:
:$X \times \set t$ admits a supremum
By definition of supremum:
:$\exists \tuple {a, b} \in S \times T: \tuple {a, b}$ is upper bound for $X \times \set t$
and:
:$\forall \tuple {c, d} \in S \times T: \tuple {c, d}$ is upper bound for $X \times \set t \implies \tuple {a, b} \preceq \tuple {c, d}$
We will prove that
:$a$ is upper bound for $X$
Let $s \in X$.
By definition of Cartesian product:
:$\tuple {s, t} \in X \times \set t$
By definition of upper bound:
:$\tuple {s, t} \preceq \tuple {a, b}$
Thus by definition of simple order product:
:$s \preceq_1 a$
We will prove that
:$\forall x \in S: x$ is upper bound for $X \implies a \preceq_1 x$
Let $x \in S$ such that
:$x$ is upper bound for $X$
We will prove as sublemma that:
:$\tuple {x, b}$ is upper bound for $X \times \set t$
Let $\tuple {y, z} \in X \times \set t$.
By definition of Cartesian product:
:$y \in X$
By definition of upper bound:
:$\tuple {y, z} \preceq \tuple {a, b}$
By definition of simple order product:
:$z \preceq_2 b$
By definition of upper bound:
:$y \preceq_1 x$
Thus by definition of simple order product:
:$\tuple {y, z} \preceq \tuple {x, b}$
This ends the proof of sublemma.
Then:
:$\tuple {a, b} \preceq \tuple {x, b}$
Thus by definition of simple order product:
:$x \preceq_1 a$
Thus by definition of supremum:
:$X$ admits a supremum:
Thus by definition:
:$\struct {S, \preceq_1}$ is up-complete.
By mutatis mutandis
:$\struct {T, \preceq_2}$ is up-complete
=== Necessary Condition ===
Assume that
:$\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ are up-complete.
Let $X$ be directed subset of $S \times T$.
By Lemma 2:
:$\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$
By definition of up-complete:
:$\map {\pr_1^\to} X$ and $\map {\pr_2^\to} X$ admit suprema
By definition of supremum:
:$\exists a \in S: a$ is upper bound for $\map {\pr_1^\to} X$
and:
:$\forall c \in S: c$ is upper bound for $\map {\pr_1^\to} X \implies a \preceq_1 c$
and
:$\exists b \in T: b$ is upper bound for $\map {\pr_2^\to} X$
and:
:$\forall c \in T: c$ is upper bound for $\map {\pr_2^\to} X \implies b \preceq_2 c$
We will prove that
:$\tuple {a, b}$ is upper bound for $X$
Let $\tuple {x, y} \in X$.
By definitions of image of set and projections:
:$x \in \map {\pr_1^\to} X$ and $y \in \map {\pr_2^\to} X$
By definition of upper bound:
:$x \preceq_1 a$ and $y \preceq_2 b$
Thus by definition of simple order product:
:$\tuple {x, y} \preceq \tuple {a, b}$
We will prove that
:$\forall \tuple {x, y} \in S \times T: \tuple {x, y}$ is upper bound for $X \implies \tuple {a, b} \preceq \tuple {x, y}$
Let $\tuple {x, y} \in S \times T$ such that:
:$\tuple {x, y}$ is upper bound for $X$
We will prove as sublemma that
:$x$ is upper bound for $\map {\pr_1^\to} X$
Let $c \in \map {\pr_1^\to} X$.
By definitions of image of set and projections:
:$\exists d: \tuple {c, d} \in X$
By definition of upper bound:
:$\tuple {c, d} \preceq \tuple {x, y}$
Thus by definition of simple order product:
:$c \preceq_1 x$
By mutatis mutandis
:$y$ is upper bound for $\map {\pr_2^\to} X$
Then:
:$a \preceq_1 x$ and $b \preceq_2 y$
Thus by definition of simple order product:
:$\tuple {a, b} \preceq \tuple {x, y}$
By definition
:$X$ admits a supremum.
Thus by definition
:$\struct {S \times T, \preceq}$ is up-complete.
== Sources ==
* 
* 
* 
Category:Order Theory