Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

## Complete Lattices

Grzegorz Bancerek
Warsaw University, Bialystok, Polish Academy of Sciences, Warsaw

### Summary.

In the first section the lattice of subsets of distinct set is introduced. The join and meet operations are, respectively, union and intersection of sets, and the ordering relation is inclusion. It is shown that this lattice is Boolean, i.e. distributive and complementary. The second section introduces the poset generated in a distinct lattice by its ordering relation. Besides, it is proved that posets which have l.u.b.'s and g.l.b.'s for every two elements generate lattices with the same ordering relations. In the last section the concept of complete lattice is introduced and discussed. Finally, the fact that the function $f$ from subsets of distinct set yielding elements of this set is a infinite union of some complete lattice, if $f$ yields an element $a$ for singleton $\{a\}$ and $f(f^\circ X) = f(\bigsqcup X)$ for every subset $X$, is proved. Some concepts and proofs are based on [8] and [9].

#### MML Identifier: LATTICE3

The terminology and notation used in this paper have been introduced in the following articles [11] [7] [14] [10] [4] [5] [3] [18] [1] [12] [2] [15] [17] [16] [6] [13]

#### Contents (PDF format)

1. Boolean lattice of subsets
2. Correspondence between lattices and posets
3. Complete lattices

#### Bibliography

[1] Grzegorz Bancerek. Filters --- part I. Journal of Formalized Mathematics, 2, 1990.
[2] Grzegorz Bancerek. Filters - part II. Quotient lattices modulo filters and direct product of two lattices. Journal of Formalized Mathematics, 3, 1991.
[3] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Helena Rasiowa and Roman Sikorski. \em The Mathematics of Metamathematics, volume 41 of \em Monografie Matematyczne. PWN, Warszawa, 1968.
[9] Tadeusz Traczyk. \em Wst\c ep do teorii algebr Boole'a, volume 37 of \em Biblioteka Matematyczna. PWN, Warszawa, 1970.
[10] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[11] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[12] Andrzej Trybulec. Finite join and finite meet, and dual lattices. Journal of Formalized Mathematics, 2, 1990.
[13] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[14] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[15] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[16] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.
[17] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Journal of Formalized Mathematics, 1, 1989.
[18] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.