Definition:Ordered Set of Increasing Mappings
Jump to navigation
Jump to search
Definition
Let $L = \struct{S_1, \preceq_1}$, $K = \struct{S_2, \preceq_2}$ be ordered sets.
The ordered set of increasing mappings from $K$ into $L$ is ordered subset of $L^{S_2} = \struct{S_1^{S_2}, \preceq'}$ and is defined by
- $\map {\operatorname{Increasing}} {K, L} = \struct{X, \precsim}$
where
- $X = \leftset {f:S_2 \to S_1: f}$ is increasing mapping$\rightset{}$
- $\mathord\precsim = \mathord\preceq' \cap \paren{X \times X}$
- $L^{S_2}$ denotes the ordered set of all mappings from $S_2$ into $L$,
- $S_1^{S_2}$ denotes the set of all mappings from $S_2$ into $S_1$.
$\map {\operatorname{Increasing}} {K, L}$ as ordered subset of ordered set is ordered set by Ordered Subset of Ordered Set is Ordered Set.
Sources
- Mizar article YELLOW_1:def 6