# Image of Directed Subset under Increasing Mapping is Directed

Jump to navigation
Jump to search

## Theorem

Let $\left({S, \preceq}\right)$, $\left({T, \precsim}\right)$ be ordered sets.

Let $f: S \to T$ be an increasing mapping.

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

Then

- $f^\to \left({D}\right)$ is also a directed subset of $T$

where

- $f^\to \left({D}\right)$ denotes the image of $D$ under $f$.

## Proof

Let $x, y \in f^\to\left({D}\right)$.

By definition of image of set:

- $\exists a \in D: x = f \left({a}\right)$

and

- $\exists b \in D: y = f \left({b}\right)$

By definition of directed subset:

- $\exists c \in D: a \preceq c \land b \preceq c$

By definition of image of set:

- $f\left({c}\right) \in f^\to\left({D}\right)$

By definition of increasing mapping:

- $x \precsim f\left({c}\right)$ and $y \precsim f\left({c}\right)$

Thus by definition

- $f^\to\left({D}\right)$ is a directed subset of $T$.

$\blacksquare$

## Sources

- Mizar article YELLOW_2:15