Continuous Lattice Subframe of Algebraic Lattice is Algebraic Lattice

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:

$P$ is an 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