Set of Infima for Sequence is Directed
Jump to navigation
Jump to search
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