Alexander's lemma

Alexander's lemma is a criterion for topological compactness in terms of covers and subbases. In [32, p. 139], it is presented as

6 THEOREM (ALEXANDER) If $\mathcal{S}$ is a subbase for the topology of a space $X$ such that every cover of $X$ by members of $\mathcal{S}$ has a finite subcover, then $X$ is compact.

The way_below relation, written as $\ll$ in the CCL-book, may be seen as a generalization of a concept related to topological compactness. It is derived from the concept of $U$ is relatively compact in $V$, for open sets $U$ and $V$ ($U$ is compact if $U$ is relatively compact in itself). This was explored in WAYBEL_3 [7] to show the correspondence between locally compact topological spaces and continuous lattices. The correspondence between way_below and topological openness and subcovers is expressed by the following lemmas

theorem                                                 :: WAYBEL_3:34 
for T being non empty TopSpace, 
    x, y being Element of InclPoset the topology of T
 st x is_way_below y
  for F being Subset-Family of the carrier of T 
   st F is open & y c= union F 
    ex G being finite Subset of F st x c= union G;

theorem                                                 :: WAYBEL_3:35 
for T being non empty TopSpace,
    x, y being Element of InclPoset the topology of T
 st for F being Subset-Family of T st F is open & y c= union F
     ex G being finite Subset of F st x c= union G
  holds x is_way_below y;

With the following definition

definition  :: CCL 1.1, p. 38
 let L be non empty reflexive RelStr, x be Element of L;
 attr x is compact means                             :: WAYBEL_3:def 2
  x is_way_below x;
 synonym x is isolated_from_below;
end;

we can state the main lemmas of interest

theorem                                                 :: WAYBEL_3:36 
for T being non empty TopSpace, 
    x being Element of InclPoset the topology of T,
    X being Subset of T st x = X 
  holds x is compact iff X is compact;

theorem                                                 :: WAYBEL_3:37
for T being non empty TopSpace,
     x being Element of InclPoset the topology of T
 st x = the carrier of T 
  holds x is compact iff T is compact;

The compact attribute on the left-hand side is defined by WAYBEL_3:def 2 and on the right-hand side it means compact in the topological sense. Pursuing this correspondence, a generalization of Alexander's lemma is given in [25, Ch. I, p. 74]

3.21. Proposition. Let $\mathcal{B}$ be a collection of open subsets forming a subbase for the topology of a space $X$, and let $U$ and $V$ be open sets with $U\subseteq V$. Then a necessary and sufficient condition for $U\ll V$ is that every cover of $V$ by members of $\mathcal{B}$ has a finite subcover of $U$.

This generalization was formalized in WAYBEL_7 [9]

theorem                                                 :: WAYBEL_7:35
 for T being non empty TopSpace, B being prebasis of T
     x, y being Element of InclPoset the topology of T
  st x c= y holds x << y
              iff
                  for F being Subset of B st y c= union F
                   ex G being finite Subset of F st x c= union G;

The mode prebasis of corresponds to the commonly used term of a subbase. Note, that the meaning of subcover is stated explicitly. Fortunately, we did not have to define the mode prebasis as it already existed in MML in CANTOR_1 [47]

definition
  let X be TopStruct;
  mode prebasis of X -> Subset-Family of X means     :: CANTOR_1:def 5 
    it c= the topology of X & 
    ex F being Basis of X st F c= FinMeetCl it;
end;

where Basis of X is

definition
  let X be TopStruct;
  mode Basis of X -> Subset-Family of X means        :: CANTOR_1:def 2
    it c= the topology of X & the topology of X c= UniCl it;

Here, UniCl and FinMeetCl of a family of sets are closures under arbitrary unions and under finite intersections, respectively.

We thought we were less fortunate with the concept of subcover since there was no corresponding definition for it in MML. The author formalizing theorem WAYBEL_7:35 struggled with the idea of defining a new mode (type constructor) for subcover of. This mode would take two arguments: a set and a family of sets. However, it turned out that in this particular theorem [25, Ch. I, 3.21], the term subcover is not used in a straightforward way: we have $U\subseteq V$, $\mathcal{B}$ is a cover of $V$, and we want to say that there exists a subcover of $U$ chosen from $\mathcal{B}$. Of course $\mathcal{B}$ is also a cover of $U$ as $U\subseteq V$. An attempt to express in MIZAR all the needed type dependencies required new notions. It also required a revision of MML as the notion of a cover was defined in COMPTS_1 for types too narrow for our needs. Instead of doing all this, the meaning of subcover was expressed directly in the theorem. The meaning of subcover is expressed very succinctly as it uses only the predicate c= and the functor union. Note that this takes the same number of characters as typing subcover! Issues like this seem to be insignificant yet they consume quite some time when one tries to be formal.

The MIZAR proof of Proposition 3.21 in [25, Ch. I] is about 8 times longer than the proof from the CCL-book (if we count words) but the reasoning is almost the same. In a MIZAR proof we must refer explicitly to all premises and inference steps are more detailed since in most cases the MIZAR checker is not as bright as most human readers.

In formal texts we have to provide an explicit analysis of all degenerate cases: empty, trivial, non proper, etc. This is one of the more significant differences between formal proofs and proofs in the CCL-book. Such analyses revealed some gaps $^{\:\alph{cclerrors}}$ in the CCL-book.

The MIZAR proof of Alexander's lemma in WAYBEL_7 [9] uses the following fact

theorem                                                 :: WAYBEL_7:30
for L being non trivial Boolean LATTICE, F being proper Filter of L
  ex G being Filter of L st F c= G & G is ultra;

which forced us to analyze some aspects of non trivial lattices. In MML, the attribute trivial has several meanings, depending on the type of the object to which it is applied, but the one relevant here concerns structures derived from 1-sorted and is defined in [16]

definition let X be set;
  attr X is trivial means                           :: REALSET1:def 12 
   X is empty or ex x being set st X = {x};
end;

definition let S be 1-sorted; 
  attr S is trivial means                           :: REALSET1:def 13
   the carrier of S is trivial;
end;

A structure that is non trivial has at least 2 elements in its carrier. Structures that are trivial have many uses since a trivial (but non empty) RelStr is the simplest object serving as a model for any lattice equality. This is used in proving correctness of existential $\mathrm{registrations}^{\:\alph{registrations}}$. In 68 existential registrations of different kinds of lattices in the YELLOW and WAYBEL series, there are 21 that use trivial RelStr as an example of existence and only 5 which employ non trivial ones (the remaining ones do not mention the adjective). There are also 18 conditional registrations stating that trivial implies some lattice properties and only 1 uses the non trivial case. It turns out that trivial things have quite non trivial uses!