Set of Infima for Sequence is Directed

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.

Let $\left({A, \precsim}\right)$ be a non-empty directed set.

Let $Z: A \to S$ be a Moore-Smith sequence.

Let $D = \left\{ {\inf \left({Z\left[{\precsim \left({j}\right)}\right]}\right): j \in A}\right\}$ be a subset of $S$.


Then $D$ is directed.


Proof

By definition of non-empty set:

$\exists j: j \in A$

By definition of $D$:

$\inf \left({Z\left[{\precsim \left({j}\right)}\right]}\right) \in D$

Hence by definition:

$D$ is a non-empty set.

Let $x, y \in D$.

By definition of $D$:

$\exists j_1 \in A: x = \inf \left({Z\left[{\precsim \left({j_1}\right)}\right]}\right)$

and

$\exists j_2 \in A: y = \inf \left({Z\left[{\precsim \left({j_2}\right)}\right]}\right)$

By definition of directed set:

$\exists j \in A: j_1 \precsim j \land j_2 \precsim j$

By Preceding implies Image is Subset of Image:

$\precsim\left({j}\right) \subseteq \mathord\precsim\left({j_1}\right)$ and $\precsim\left({j}\right) \subseteq \mathord\precsim\left({j_2}\right)$

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

$Z\left[{\precsim\left({j}\right)}\right] \subseteq Z\left[{\precsim\left({j_1}\right)}\right]$ and $Z\left[{\precsim\left({j}\right)}\right] \subseteq Z\left[{\precsim\left({j_2}\right)}\right]$

Thus by definition of $D$:

$z := \inf \left({Z\left[{\precsim \left({j}\right)}\right]}\right) \in D$

Thus by Infimum of Subset:

$x \preceq z$ and $y \preceq z$

$\blacksquare$


Sources