Set of Upper Closures of Compact Elements is Basis implies Complete Scott Topological Lattice is Algebraic

From ProofWiki
Jump to navigation Jump to search


Let $L = \struct {S, \preceq, \tau}$ be a complete Scott Definition:Topological Lattice.

Let $\BB = \left\{ {x^\succeq: x \in K\left({L}\right)}\right\}$ be a basis of $L$


$x^\succeq$ denotes the upper closure of $x$,
$K\left({L}\right)$ denotes the compact subset of $L$.

Then $L$ is algebraic.


Thus by Compact Closure is Directed:

$\forall x \in S:x^{\mathrm{compact} }$ is directed

where $x^{\mathrm{compact} }$ denotes the compact closure of $x$.

Thus by definition of complete lattice:

$L$ is up-complete.

Let $x \in S$.

By definition of lower closure of element:

$x$ is upper closure for $x^\preceq$

By definition of supremum:

$\sup \left({x^\preceq}\right) \preceq x$

By Compact Closure is Intersection of Lower Closure and Compact Subset:

$x^{\mathrm{compact} } = x^\preceq \cap K\left({L}\right)$

By Intersection is Subset:

$x^{\mathrm{compact} } \subseteq x^\preceq$

By Supremum of Subset:

$\sup \left({x^{\mathrm{compact} } }\right) \preceq \sup \left({x^\preceq}\right)$

By definition of transitivity:

$\sup \left({x^{\mathrm{compact} } }\right) \preceq x$

Aiming for a contradiction, suppose

$x \ne \sup \left({x^{\mathrm{compact} } }\right)$

We will prove that

$x \notin \left({\left({x^{\mathrm{compact} } }\right) }\right)^\preceq$

Aiming for a contradiction, suppose

$x \in \left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq$

By definition of lower closure of element:

$x \preceq \sup \left({x^{\mathrm{compact} } }\right)$

Thus by definition of antisymmetry:

this contrasicts $x \ne \sup \left({x^{\mathrm{compact} } }\right)$


By definition of relative complement:

$x \in \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$

By Complement of Lower Closure of Element is Open in Scott Topological Ordered Set:

$\complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$ is open.

By definition of basis:

$\complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right) = \bigcup\left\{ {G \in \BB: G \subseteq \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)}\right\}$

By definition of union

$\exists X \in \left\{ {G \in \BB: G \subseteq \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)}\right\}: x \in X$


$X \in \BB \land X \subseteq \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$

By definition of $\BB$:

$\exists k \in K\left({L}\right): X = k^\succeq$

By definition of compact subset:

$k$ is compact.

By definition of upper closure of element:

$k \preceq x$

By definition of compact closure:

$k \in x^{\mathrm{compact} }$

By definitions of supremum and upper bound:

$k \preceq \sup \left({x^{\mathrm{compact} } }\right)$

By definition of upper closure of element:

$\sup \left({x^{\mathrm{compact} } }\right) \in X$

By gefinition of subset:

$\sup \left({x^{\mathrm{compact} } }\right) \in \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$

By definition of difference:

$\sup \left({x^{\mathrm{compact} } }\right) \notin \left({\sup \left({x^{\mathrm{compact} } }\right)}\right)^\preceq$

Thus by definition of lower closure of element:

this contradicts $\sup \left({x^{\mathrm{compact} } }\right) \in \left({\sup \left({x^{\mathrm{compact} } }\right)}\right)^\preceq$