next up previous
Next: State of formalization and Up: Lim-inf convergence and its Previous: Lim-inf convergence

Proof of compactness

The last theorem in [W33], theorem (27), states

Every complete lim-inf top-lattice is compact and $T_1$.
To prove the first part of it, we used one of the characterizations of compactness given in theorem (33) of [Y19]:
A non empty topological space $T$ is compact if and only if for every ultra filter $F$ of $2^{\Omega_T}_\subseteq$ there exists a point of $T$ which is a convergence point of $F$ in $T$.
$\Omega_T$ is the carrier of $T$ treated as a subset of $T$. We showed that the convergence point of the filter $F$ of our complete lim-inf top-lattice was
$\mathop{\underline\lim}F = \sup_{A \in F} \inf A$
First, let us note theorem (13) in [W33], which states that $\mathop{\underline\lim}F = \mathop{\underline\lim}N_F$, where $N_F$ is the net of a proper filter $F$.

Next, all subnets of $N_F$, the net of an ultra filter $F$, have the same lower limit as the net $N_F$ ([W33, (16)]). So, the pair $(N_F, \mathop{\underline\lim}F)$ is in the lim-inf convergence of $T$.

Finally, closed sets can be characterized by the condition [W33, (18)]: a subset $A$ of a complete lim-inf top-lattice is closed if and only if for every ultra filter $F$, if $A \in F$, then $\mathop{\underline\lim}F \in A$. The proof of the implication from the left side to the right (we need only this) may be sketched as follows: Suppose that $-A$ is open and that $F$ is an ultra filter with $A \in F$. Moreover, suppose (ad absurdum) that $\mathop{\underline\lim}F \not\in A$. That is, $\mathop{\underline\lim}N_F \in -A$ and $N_F$ is eventually in $-A$ because the pair $(N_F, \mathop{\underline\lim}F)$ is from the lim-inf convergence and $-A$ is an element of the topology induced by the lim-inf convergence. This means that there exists a pair $(x, B)$ which is an index of $N_F$ such that all values of $N_F$ for indices larger than $(x, B)$ are from $-A$. Point $x \in B$ and $B \in F$. According to the condition of the ultra filter, $A\cap B \in F$ and $y \in A \cap B$ for some point $y$. A pair $(y, A \cap B)$ is an index of $N_F$ larger than $(x, B)$ because $A\cap B \subseteq B$. Then,

\begin{displaymath}
y = N_F(y, A \cap B) \in -A \qquad{\rm and}\qquad
y \in A \cap B \subseteq A
\end{displaymath}

which end the proof of the implication.

Now, the proof of the fact that $\mathop{\underline\lim}F$ is a convergence point of $F$ is simple. Let $A$ be an open neighborhood of $\mathop{\underline\lim}F$ and assume, ad absurdum, that $A \not\in F$. Then, $-A \in F$ because $F$ is prime as an ultra filter in a Boolean lattice. $-A$ is a closed set, so $\mathop{\underline\lim}F \in -A$, which contradicts with $\mathop{\underline\lim}F \in A$.


next up previous
Next: State of formalization and Up: Lim-inf convergence and its Previous: Lim-inf convergence
Grzegorz Bancerek 2002-03-15