Definition:Increasing Mappings Satisfying Inclusion in Lower Closure

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

• Correctness of Definition of Increasing Mappings Satisfying Inclusion in Lower Closure

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