Way Below iff Second Operand Preceding Supremum of Directed Set There Exists Element of Directed Set First Operand Way Below Element
Jump to navigation
Jump to search
Theorem
Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.
Let $x, y$ be elements of $S$.
Then
- $x \ll y$
- for every directed subset $D$ of $S$ such that $y \preceq \sup D$
- there exists an element $d$ of $D$: $x \ll d$
Proof
Sufficient Condition
Let $x \ll y$.
Let $D$ be a directed subset of $S$ such that
- $y \preceq \sup D$
By Way Below has Interpolation Property:
- $\exists x' \in S: x \ll x' \land x' \ll y$
By definition of way below relation:
- $\exists d \in D: x' \preceq d$
Thus by Preceding and Way Below implies Way Below and definition of reflexivity:
- $x \ll d$
$\Box$
Necessary Condition
Assume that
- for every directed subset $D$ of $S$ such that $y \preceq \sup D$
- there exists an element $d$ of $D$: $x \ll d$
By Way Below implies Preceding:
- for every directed subset $D$ of $S$ such that $y \preceq \sup D$
- there exists an element $d$ of $D$: $x \preceq d$
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_4:53