Way Below is Approximating Relation
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Then $\ll$ is an approximating relation on $S$.
Proof
Let $x \in S$.
Define $\RR := \mathord \ll$.
By definitions of way below closure and $\RR$-segment:
- $x^\ll = x^\RR$
where:
- $x^\ll$ denotes the way below closure of $x$
- $x^\RR$ denotes the $\RR$-segment of $x$
By definition of continuous:
- $L$ satisfies the axiom of approximation.
Thus by the axiom of approximation:
- $x = \map \sup {x^\ll} = \map \sup {x^\RR}$
Hence $\ll$ is an approximating relation on $S$.
$\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:Lm12