Definition:Increasing Mappings Satisfying Inclusion in Lower Closure
Jump to navigation
Jump to search
Definition
Let $R = \struct {S, \preceq}$ be an ordered set.
Let $\map {\it Ids} R$ be the set of all ideals in $R$.
Let $L = \struct {\map {\it Ids} R, \precsim}$ be an ordered set where $\precsim \mathop = \subseteq \restriction_{\map {\it Ids} R \times \map {\it Ids} R}$
Then the ordered set $M$ of increasing mappings $f: R \to L$ satisfying $\forall x \in S: \map f x \subseteq x^\preceq$
is defined by:
- $M = \struct {F, \preccurlyeq}$
where:
- $F = \leftset {f: S \to \map {\it Ids} R: f}$ is increasing mapping $\rightset {\land \forall x \in S: \map f x \subseteq x^\preceq}$
and:
- $\preccurlyeq$ is ordering on mappings generated by $\precsim$
where $x^\preceq$ denotes the lower closure of $x$.
Also see
Sources
- 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices
- Mizar article WAYBEL_4:def 13