Subset and Image Admit Infima and Mapping is Increasing implies Infimum of Image Succeeds Mapping at Infimum

Theorem

Let $\struct {S, \preceq}$ and $\struct {T, \precsim}$ be ordered sets.

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

Let $D \subseteq S$ such that

$D$ admits a infimum in $S$ and $f \sqbrk D$ admits a infimum in $T$.

Then $\map f {\inf D} \precsim \map \inf {f \sqbrk D}$

Proof

By definition of infimum:

$\inf D$ is lower bound for $D$.

By Increasing Mapping Preserves Lower Bounds:

$\map f {\inf D}$ is a lower bound for $f \sqbrk D$.

Thus by definition of infimum:

$\map f {\inf D} \precsim \map \inf {f \sqbrk D}$

$\blacksquare$

Sources

• Mizar article WAYBEL17:17