Continuous Lattice Subframe of Algebraic Lattice is Algebraic Lattice
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Let $P = \struct {T, \precsim}$ be a continuous lattice subframe of $L$.
Then $P$ is algebraic lattice.
Proof
By definition of algebraic ordered set:
- $L$ is up-complete.
By Up-Complete Lower Bounded Join Semilattice is Complete:
- $L$ is a complete lattice.
By definition:
- $P$ is closure system of $L$.
By Image of Operator Generated by Closure System is Set of Closure System
- $\map {\operatorname {operator} } P \sqbrk S = T$
By Closure Operator Preserves Directed Suprema iff Image of Closure Operator Inherits Directed Suprema
- $\map {\operatorname {operator} } P$ preserves directed suprema.
Thus by Image of Directed Suprema Preserving Closure Operator is Algebraic Lattice:
$\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 WAYBEL13:6