# Mapping at Limit Inferior Precedes Limit Inferior of Composition Mapping and Sequence implies Supremum of Image is Mapping at Supremum of Directed Subset

## Theorem

Let $\left({S, \vee_1, \wedge_1, \preceq_1}\right)$ and $\left({T, \vee_2, \wedge_2, \preceq_2}\right)$ be up-complete lattices.

Let $f: S \to T$ be a mapping such that

- for all directed set $\left({D, \precsim}\right)$ and Moore-Smith sequence $N:D \to S$ in $S$: $f\left({\liminf N}\right) \preceq_2 \liminf\left({f \circ N}\right)$

Let $D$ be a directed subset of $S$.

Then $\sup \left({f\left[{D}\right]}\right) = f\left({\sup D}\right)$

where $f\left[{D}\right]$ denotes the image of $D$ under $f$.

## Proof

- $f$ is an increasing mapping.

By Image of Directed Subset under Increasing Mapping is Directed:

- $f\left[{D}\right]$ is directed.

By definition of up-complete:

- $D$ and $f\left[{D}\right]$ admit suprema.

- $\sup \left({f\left[{D}\right]}\right) \preceq_2 f\left({\sup D}\right)$

By Limit Inferior of Inclusion Moore-Smith Sequence is Supremum of Directed Subset:

- $\sup D = \liminf i_D$

By assumption:

- $f\left({\sup D}\right) \preceq_2 \liminf \left({f \circ i_D}\right)$

By Composition of Mapping and Inclusion is Restriction of Mapping:

- $f \circ i_D = f\restriction{D}$

By Limit Inferior of Restriction Moore-Smith Sequence is Supremum of Image of Directed Subset:

- $\sup \left({f\left[{D}\right]}\right) = \liminf \left({f \circ i_D}\right)$

Then

- $f\left({\sup D}\right) \preceq_2 \sup \left({f\left[{D}\right]}\right)$

Thus by definition of antisymmetry:

- $\sup \left({f\left[{D}\right]}\right) = f\left({\sup D}\right)$

$\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 WAYBEL17:19