Definition:Inclusion Ordered Set
Jump to navigation
Jump to search
Definition
Let $\struct {S, \preceq}$ be an ordered set.
$\struct {S, \preceq}$ is inclusion ordered set if and only if:
- $\mathord\preceq = \mathord\subseteq \cap \paren {S \times S}$
That means:
- $\forall x, y \in S: x \preceq y \iff x \subseteq y$
Sources
- Mizar article YELLOW_1:def 1