Supremum of Ideals is Increasing

Theorem

Let $L = \left({S, \preceq}\right)$ be an up-complete ordered set.

Let $\mathit{Ids}\left({L}\right)$ be the set of all ideals in $L$.

Let $P = \left({\mathit{Ids}\left({L}\right), \precsim}\right)$ be an ordered set where $\mathord \precsim = \subseteq\restriction_{\mathit{Ids}\left({L}\right)\times \mathit{Ids}\left({L}\right)}$

Let $f: \mathit{Ids}\left({L}\right) \to S$ be a mapping such that

$\forall I \in \mathit{Ids}\left({L}\right): f\left({I}\right) = \sup I$

Then $f$ is an increasing mapping.

Proof

Let $I, J \in \mathit{Ids}\left({L}\right)$ such that

$I \precsim J$

By definition of $\precsim$:

$I \subseteq J$

By definition of up-complete:

$I$ and $J$ admit suprema in $L$.

By Supremum of Subset:

$\sup I \preceq \sup J$

Thus by definition of $f$:

$f\left({I}\right) \preceq f\left({J}\right)$

Hence $f$ is an increasing mapping.

$\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 YELLOW_2:51