Upper Closure is Compact in Topological Lattice
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \preceq, \tau}$ be a topological lattice.
Suppose that:
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$
- $\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$.
- $\GG$ is finite.
Thus by definition:
- $\GG$ is finite subcover of $\FF$.
$\blacksquare$
Sources
- Mizar article WAYBEL14:22