Image of Mapping of Infima is Generator Set of Filter

Theorem

Let $\left({S, \wedge, \preceq}\right)$ be a meet semilattice.

Let $f, g:\N \to S$ be mappings such that

$\forall n \in \N: g\left({n}\right) = \inf \left\{ {f\left({m}\right): m \in \N \land m \le n}\right\}$

Let $F$ be a filter such that

$f\left[{\N}\right]$ is generator set of $F$,

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

Then $g\left[{\N}\right]$ is generator set of $F$.

$f\left[{\N}\right]$ is coarser than $g\left[{\N}\right]$.

$F = \left({\operatorname{fininfs}\left({f\left[{\N}\right]}\right)}\right)^\succeq$

where

$\operatorname{fininfs}\left({f\left[{\N}\right]}\right)$ denotes the finite infima set of $f\left[{\N}\right]$,

for subset $A$ of $S$: $A^\succeq$ denotes upper closure of $A$.

$f\left[{\N}\right] \subseteq F$

We will prove that

$g\left[{\N}\right] \subseteq F$

Let $x \in g\left[{\N}\right]$.

By definition of image of mapping:

$\exists n \in \N: x = g\left({n}\right)$

By definition of $g$:

$x = \inf \left\{ {f\left({m}\right): m \in \N \land m \le n}\right\}$

By definition:

$\left\{ {f\left({m}\right): m \in \N \land m \le n}\right\}$ is a finite set.

By definition of subset:

$\left\{ {f\left({m}\right): m \in \N \land m \le n}\right\} \subseteq F$

By definition of reflexivity:

$f\left({n}\right) \in \left\{ {f\left({m}\right): m \in \N \land m \le n}\right\}$

$x \in F$

$\Box$

$g\left[{\N}\right]$ is coarser than $F$.

$g\left[{\N}\right]$ is generator set of $F$.

$\blacksquare$