User:Dfeuer/Product Order is Order
This page has been identified as a candidate for refactoring. In particular: Put this live as Simple Order Product of Family of Ordered Sets is Ordered Set Until this has been finished, please leave {{Refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code. |
Theorem
Let $\struct {S_i, \preceq_i}$ be an ordered set for each $i \in I$.
Let $\preceq$ be the User:Dfeuer/Definition:Product Order on:
- $S = \ds \prod_{i \mathop \in I} S_i$
Then $\struct {S, \preceq}$ is an ordered set.
Proof
$\preceq$ is reflexive:
Let $x \in S$.
Since $\preceq_i$ is reflexive for each $i \in I$, $x_i \preceq_i x_i$ for each $i \in i$.
Thus by the definition of the product order, $x \preceq x$.
$\preceq$ is transitive:
Suppose that $x \preceq y$ and $y \preceq z$.
Then by the definition of the product order, for each $i \in I$, $x_i \preceq_i y_i$ and $y_i \preceq_i z_i$.
Since each $\preceq_i$ is transitive,
for each $i \in I$, $x_i \preceq_i z_i$.
Thus, by the definition of the product order, $x \preceq z$.
$\preceq$ is antisymmetric:
Suppose that $x \preceq y$ and $y \preceq x$.
By the definition of the product order, for each $i \in I$, $x_i \preceq_i y_i$ and $y_i \preceq_i x_i$.
Since each $\preceq_i$ is anti-symmetric, for each $i \in I$, $x_i = y_i$.
By the definition of cartesian product, $x = y$.
$\blacksquare$