Upper Closure is Compact in Topological Lattice

Theorem

Let $L = \struct {S, \preceq, \tau}$ be a topological lattice.

Suppose that:

for every subset $X$ of $S$ if $X$ is open, then $X$ is upper.

Let $x \in S$.

Then $x^\succeq$ is compact

where $x^\succeq$ denotes the upper closure of $x$.

Proof

Let $\FF$ be a set of subsets of $S$ such that:

$\FF$ is open cover of $x^\succeq$

By definition of cover:

$x^\succeq \subseteq \bigcup \FF$

By definitions of upper closure of element and reflexivity:

$x \in x^\succeq$

By definition of subset:

$x \in \bigcup \FF$

By definition of union:

$\exists Y \in \FF: x \in Y$

Define $\GG = \set Y$.

By definition of open cover:

$Y$ is open.

We will prove that:

$x^\succeq \subseteq \bigcup \GG$

Let $y \in x^\succeq$.

By definition of upper closure of element:

$x \preceq y$

By Union of Singleton:

$\bigcup \GG = Y$

By assumption:

$Y$ is upper.

Thus by definition of upper section:

$x \in \bigcup \GG$

$\Box$

Then by definition:

$\GG$ is cover of $x^\succeq$

By definitions of singleton and subset:

$\GG \subseteq \FF$

By definition:

$\GG$ is subcover of $\FF$.

By Singleton is Finite:

$\GG$ is finite.

Thus by definition:

$\GG$ is finite subcover of $\FF$.

$\blacksquare$

Sources

• Mizar article WAYBEL14:22