Way Below iff Preceding Finite Supremum
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$ if and only if
- $\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\it Fin} X: x \preceq \sup A$
where
- $\ll$ denotes the way below relation,
- $\map {\it 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$
Define:
- $F := \set {\sup A: A \in \map {\it Fin} X}$
By definition of union:
- $X = \bigcup \map {\it Fin} X$
- $\sup X = \sup F$
We will prove that:
- $F$ is directed
Let $a, b \in F$.
By definition of $F$:
- $\exists A \in \map {\it Fin} X: a = \sup A$
and
- $\exists B \in \map {\it Fin} X: b = \sup B$
By Union of Subsets is Subset:
- $A \cup B \subseteq X$
By Finite Union of Finite Sets is Finite:
- $A \cup B$ is finite
By definition of ${\it Fin}$:
- $A \cup B \in \map {\it Fin} X$
By definition of $F$:
- $\map \sup {A \cup B} \in F$
- $A \subseteq A \cup B$ and $B \subseteq A \cup B$
- $a \preceq \map \sup {A \cup B}$ and $b \preceq \map \sup {A \cup B}$
Thus by definition:
- $F$ is directed
By definition of way below relation:
- $\exists d \in F: x \preceq d$
Thus by definition of $F$:
- $\exists A \in \map {\it Fin} X: x \preceq \sup A$
$\Box$
Necessary Condition
Assume that:
- $\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\it 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 {\it Fin} D: x \preceq \sup A$
By Directed iff Finite Subsets have Upper Bounds:
- $\exists h \in D: \forall a \in A: a \preceq h$
By definition:
- $h$ is upper bound for $A$
By definition of supremum:
- $\sup A \preceq h$
Thus by definition of transitivity:
- $x \preceq h$
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