Definition:Ordered Subset

Definition

Let $R = \struct{S, \preceq}$ be a relational structure.

Leigh.Samphier suggests: The validity of the material on this page is questionable. In particular: A relational substructure of a relational structure is not necessarily ordered. So either: (a) $\struct{S, \preceq}$ needs to be ordered; (b) $\struct{S', \preceq'}$ needs to be ordered; or (c) the page needs to be renamed. The theorem Ordered Subset of Ordered Set is Ordered Set and many links to the page suggests (a) is needed. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues. 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 {{Questionable}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

A ordered subset of $R$ is a relational structure $\struct{S', \preceq'}$ such that

$S'$ is a subset of $S$,

$\mathord\preceq' = \mathord\preceq \cap \paren{S' \times S'}$

That is

$\forall x, y \in S': x \preceq y \iff x \preceq' y$

Sources

• Mizar article YELLOW_0:def 13

• Mizar article YELLOW_0:def 14