Mapping Preserves Finite and Filtered Infima

Theorem

Let $\left({S_1, \preceq_1}\right)$, $\left({S_2, \preceq_2}\right)$ be meet semilattices.

Let $f: S_1 \to S_2$ be a mapping.

Let $f$ preserve finite infima and preserve filtered infima.

Then $f$ also preserves all infima

Proof

Assume that

$(1): \quad f$ preserves finite infima

and

$(2): \quad f$ preserves filtered infima.

Let $X$ be a subset of $S_1$.

Let $X$ admits an infimum in $\left({S_1, \preceq_1}\right)$

Define $Z := \left\{ {\inf A: A \in {\it Fin}\left({X}\right) \land A \ne \varnothing}\right\}$

where

$\inf A$ denotes the infimum of $A$ in $\left({S_1, \preceq_1}\right)$

${\it Fin}\left({X}\right)$ denotes the set of all finite subsets of $X$

By Existence of Non-Empty Finite Infima in Meet Semilattice:

for every non-empty finite subset $A$ of $X$, $A$ admits an infimum in $\left({S_1, \preceq_1}\right)$

By Infimum of Infima:

$\inf Z = \inf\bigcup \left({ {\it Fin}\left({X}\right) \setminus \left\{ {\varnothing}\right\} }\right) = \inf X$

$Z$ admits an infimum in $\left({S_1, \preceq_1}\right)$

We will prove that

$Z$ is filtered

Let $x, y \in Z$.

By definition of $Z$:

$\exists A \in {\it Fin}\left({X}\right) \setminus \left\{ {\varnothing}\right\}: x = \inf A$

and

$\exists B \in {\it Fin}\left({X}\right) \setminus \left\{ {\varnothing}\right\}: y = \inf B$

By Finite Union of Finite Sets is Finite:

$A \cup B$ is finite

$A \cup B \ne \varnothing$

By definition of $Z$:

$\inf\left({A \cup B}\right) \in Z$

By Infimum of Infima:

$\left({\inf A}\right) \wedge \left({\inf B}\right) = \inf\left({A \cup B}\right)$

Thus by definition of infimum:

$\inf\left({A \cup B}\right) \preceq_1 x \land \inf\left({A \cup B}\right) \preceq_1 y$

Thus by definition

$Z$ is filtered

By $(2)$ and definitions of mapping preserves filtered infima and mapping preserves infimum on subset:

$f^\to\left({Z}\right)$ admits an infimum in $\left({S_2, \preceq_2}\right)$ and $\inf\left({f^\to\left({Z}\right)}\right) = f\left({\inf Z}\right)$

We will prove that

$X \subseteq Z$

Let $x \in X$.

By definition of ${\it Fin}\left({X}\right)$:

$\left\{ {x}\right\} \in {\it Fin}\left({X}\right)$ and $\left\{ {x}\right\} \ne \varnothing$

By definition of $Z$:

$\inf \left\{ {x}\right\} \in Z$

Thus by Infimum of Singleton:

$x \in Z$

By Image of Subset under Relation is Subset of Image/Corollary 2:

$f^\to\left({X}\right) \subseteq f^\to\left({Z}\right)$

By definition of infimum:

$\inf\left({f^\to\left({Z}\right)}\right)$ is a lower bound for $f^\to\left({Z}\right)$

By Lower Bound is Lower Bound for Subset

$\inf\left({f^\to\left({Z}\right)}\right)$ is a lower bound for $f^\to\left({X}\right)$

We will prove that

for every lower bound $a$ for $f^\to\left({X}\right)$, $a$ is lower bound for $f^\to\left({Z}\right)$

Assume that

$a$ is lower bound for $f^\to\left({X}\right)$

Let $x \in f^\to\left({Z}\right)$.

By definition of image of set:

$\exists y \in S_1: y \in Z \land f\left({y}\right) = x$

By definition of $Z$:

$\exists A \in {\it Fin}\left({X}\right): y = \inf A \land A \ne \varnothing$

By $(1)$ and definition of mapping preserves finite infima:

$f$ preserves the infimum of $A$

By Existence of Non-Empty Finite Infima in Meet Semilattice

$A$ admits an infimum in $\left({S_1, \preceq_1}\right)$ and $\inf\left({f^\to\left({A}\right)}\right) = f\left({\inf A}\right) = x$

By Image of Subset under Relation is Subset of Image/Corollary 2:

$f^\to\left({A}\right) \subseteq f^\to\left({X}\right)$

By Lower Bound is Lower Bound for Subset

$a$ is lower bound for $f^\to\left({A}\right)$

Thus by definition of infimum:

$a \preceq_2 x$

Thus by definition

$a$ is lower bound for $f^\to\left({Z}\right)$

By definition of infimum:

for every lower bound $a$ for $f^\to\left({X}\right)$, $a \preceq_2 f\left({\inf X}\right)$

Again by definition of infimum:

$f^\to\left({X}\right)$ admits an infimum in $\left({S_2, \preceq_2}\right)$

$\inf\left({f^\to\left({X}\right)}\right) = f\left({\inf X}\right)$

Thus the result follows by definition of mapping preserves all infima.

$\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 WAYBEL_0:71