# Extension of Directed Suprema Preserving Mapping to Complete Lattice Preserves Directed Suprema

Jump to navigation
Jump to search

## Theorem

Let $L_1 = \left({S_1, \preceq_1}\right)$, $L_2 = \left({S_2, \preceq_2}\right)$ be ordered sets.

Let $L_3 = \left({S_3, \preceq_3}\right)$ be a complete lattice.

Suppose that

- $L_2$ is directed suprema inheriting ordered subset of $L_3$.

Let $f:S_1 \to S_2$ be a mapping such that

Then
$f:S_1 \to S_3$ preserves directed suprema.

## Proof

By definition of ordered subset:

- $S_2 \subseteq S_3$

Then define $g = f:S_1 \to S_3$

Let $X$ be a directed subset of $S_1$ such that

- $X$ admits a supremum in $L_1$.

Thus by definition of complete lattice:

- $g\left[{X}\right]$ admits a supremum in $L_3$.

By definition of mapping preserves directed suprema:

- $f\left[{X}\right]$ admits a supremum in $L_2$ and $\sup_{L_2} \left({f\left[{X}\right]}\right) = f\left({\sup_{L_1} X}\right)$

By Directed Suprema Preserving Mapping is Increasing:

- $f$ is an increasing mapping.

By Image of Directed Subset under Increasing Mapping is Directed:

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

Thus by definition of directed suprema inheriting:

- $\inf_{L_3} \left({g\left[{X}\right]}\right) = g\left({\inf_{L_1} X}\right)$

$\blacksquare$

## Sources

- Mizar article WAYBEL13:22