Lim-inf convergence and its compactness

Grzegorz Bancerek¹

Institute of Computer Science
Biaystok Technical University
Biaystok, Poland
bancerek@mizar.org - Noboru Endou

Gifu National College
of Technology
Gifu, Japan
endo-n@gifu-nct.ac.jp - Yasunari Shidama

Dept. of Information Engineering
Shinshu University
Nagano, Japan
shidama@cs.shinshu-u.ac.jp

Abstract - We describe the Mizar formalization of the proof of compactness of lim-inf convergence given in [W33] according to [CCL]. Lim-inf convergence formalized in [W28] is a Moore-Smith convergence investigated in [Y6] and involves the concept of nets. The proof is based on the equivalence of two approaches to convergence in topological spaces: filter convergence and Moore-Smith (net) convergence. The equivalence is worked out in [Y19] and different characterizations of compactness are also given there.

These efforts are a continuation of the international project of formalization of the theory of continuous lattices headed by the first author.

Keywords - formalized mathematics, continuous lattices, Scott and Lawson topologies, Moore-Smith and filter convergence, compactness.