Way Above Closures Form Basis

Theorem

Let $L = \struct {S, \preceq, \tau}$ be a complete continuous topological lattice with Scott topology.

Then $\set {x^\gg: x \in S}$ is an (analytic) basis of $L$.

Proof

Define $B = \set {x^\gg: x \in S}$.

Thus by Way Above Closure is Open:

$B \subseteq \tau$

We will prove that:

for all $x \in S$: there exists a local basis $Q$ of $x$: $Q \subseteq B$

Let $x \in S$.

By Way Above Closures that Way Below Form Local Basis:

$Q := \set {g^\gg: g \in S \land g \ll x}$ is a local basis at $x$.

Thus by definition of subset:

$Q \subseteq B$

$\Box$

Thus by Characterization of Analytic Basis by Local Bases:

$B$ is an (analytic) basis of $L$.

$\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 WAYBEL11:45