Correctness of Definition of Increasing Mappings Satisfying Inclusion in Lower Closure

Theorem

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}$

Let:

$M = \struct {F, \preccurlyeq}$

where:

$F = \leftset {f: S \to \map {\it Ids} R: f} \,$ is an increasing mapping and $\rightset {\forall x \in S: \map f x \subseteq x^\preceq}$

$\preccurlyeq$ is ordering on mappings generated by $\precsim$

$x^\preceq$ denotes the lower closure of $x$.

Then $M$ is an ordered set.

Proof

Reflexivity

Let $f \in F$.

By definition of reflexivity:

$\forall x \in S: \map f x \precsim \map f x$

Thus by definition of ordering on mappings:

$f \preccurlyeq f$

$\Box$

Transitivity

Let $f, g, h \in F$ such that

$f \preccurlyeq g \preccurlyeq h$

By definition of ordering on mappings:

$\forall x \in S: \map f x \precsim \map g x \precsim \map h x$

By definition of transitivity:

$\forall x \in S: \map f x \precsim \map h x$

Thus by definition of ordering on mappings:

$f \preccurlyeq h$

$\Box$

Antisymmetry

Let $f, g \in F$ such that

$f \preccurlyeq g$ and $g \preccurlyeq f$

By definition of ordering on mappings:

$\forall x \in S: \map f x \precsim \map g x \land \map g x \precsim \map f x$

By definition of antisymmetry:

$\forall x \in S: \map f x = \map g x$

Thus by equality of mappings:

$f = g$

$\Box$

Thus by definition:

$M$ is an ordered set.

$\blacksquare$

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