Set of Infima for Sequence is Directed

Theorem

Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.

Let $\struct {A, \precsim}$ be a non-empty directed set.

Let $Z: A \to S$ be a net.

Let $D = \set {\map \inf {Z \sqbrk {\map \precsim j} }: j \in A}$ 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 \sqbrk {\map \precsim j} }\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 = \map \inf {Z \sqbrk {\map \precsim {j_1} } }$

and

$\exists j_2 \in A: y = \map \inf {Z \sqbrk {\map \precsim {j_2} } }$

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:

$\map \precsim j \subseteq \map {\mathord \precsim} {j_1}$ and $\map \precsim j \subseteq \map {\mathord \precsim} {j_2}$

By Image of Subset under Mapping is Subset of Image:

$Z \sqbrk {\map \precsim j} \subseteq Z \sqbrk {\map \precsim {j_1} }$ and $Z \sqbrk {\map \precsim j} \subseteq Z \sqbrk {\map \precsim {j_2} }$

Thus by definition of $D$:

$z := \map \inf {Z \sqbrk {\map \precsim j} } \in D$

Thus by Infimum of Subset:

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

$\blacksquare$

Sources

• Mizar article WAYBEL11:30