Way Below in Complete Lattice
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$.
Then
- $x \ll y$
- $\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
where
- $\ll$ denotes the way below relation,
- $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.
Proof
Sufficient Condition
Let
- $x \ll y$
Let $X \subseteq S$ such that
- $y \preceq \sup X$
By Set of Finite Suprema is Directed:
- $\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
By definition of union:
- $\bigcup \map {\operatorname {Fin} } X \setminus \set \O = X$
- $\sup X = \sup \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
By definition of way below relation:
- $\exists z \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}: x \preceq z$
Thus
- $\exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
$\Box$
Necessary Condition
Let
- $\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
Let $D$ be a directed subset of $S$ such that
- $y \preceq \sup D$
By assumption:
- $\exists A \in \map {\operatorname {Fin} } D: x \preceq \sup A$
By Directed iff Finite Subsets have Upper Bounds:
- $\exists u \in D: u$ is upper bound for $A$
By definition of supremum:
- $\sup A \preceq u$
Thus by definition of transitivity:
- $x \preceq u$
Thus by definition of way below relation:
- $x \ll y$
$\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_3:18
- Mizar article WAYBEL_3:19