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

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.