Supremum of Simple Order Product

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ be ordered sets.

Let $\struct {S_1 \times S_2, \precsim}$ be the simple order product of $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$.

Let $X_1$ be a non-empty subset of $S_1$, $X_2$ be a non-empty subset of $S_2$ such that

$X_1$ and $X_2$ admit suprema.

Then:

$X_1 \times X_2$ admits a supremum

and:

$\map \sup {X_1 \times X_2} = \tuple {\sup X_1, \sup X_2}$


Proof

We will prove that:

$\tuple {\sup X_1, \sup X_2}$ is upper bound for $X_1 \times X_2$

Let $\tuple {a, b} \in X_1 \times X_2$.

By definition of Cartesian product:

$a \in X_1$ and $b \in X_2$

By definitions of supremum and upper bound:

$a \preceq_1 \sup X_1$ and $b \preceq_2 \sup X_2$

Thus by definition of simple order product:

$\tuple {a, b} \precsim \tuple {\sup X_1, \sup X_2}$

$\Box$


We will prove that:

$\forall \tuple {a, b} \in S1 \times S_2: \tuple {a, b}$ is upper bound for $X_1 \times X_2 \implies \tuple {\sup X_1, \sup X_2} \precsim \tuple {a, b}$

Let $\tuple {a, b} \in S1 \times S_2$ such that:

$\tuple {a, b}$ is upper bound for $X_1 \times X_2$

We will prove as sublemma that:

$a$ is upper bound for $X_1$

Let $c \in X_1$.

By definition of non-empty set:

$\exists d: d \in X_2$

By definition of Cartesian product:

$\tuple {c, d} \in X_1 \times X_2$

By definition of upper bound:

$\tuple {c, d} \precsim \tuple {a, b}$

Thus by definition of simple order product:

$c \preceq_1 a$

This ends the proof of sublemma.


Analogically we have that:

$b$ is upper bound for $X_2$

By definition of supremum:

$\sup X_1 \preceq_1 a$ and $\sup X_2 \preceq_2 b$

Thus by definition of simple order product:

$\tuple {\sup X_1, \sup X_2} \precsim \tuple {a, b}$

$\Box$


Thus by definition:

$X_1 \times X_2$ admits a supremum

and:

$\map \sup {X_1 \times X_2} = \tuple {\sup X_1, \sup X_2}$

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Supremum_of_Simple_Order_Product&oldid=533576"