The Equational Characterization of Continuous Lattices

Mariusz Zynel

Warsaw University, Bialystok

Summary.

The class of continuous lattices can be characterized by infinitary equations. Therefore, it is closed under the formation of subalgebras and homomorphic images. Following the terminology of [18] we introduce a continuous lattice subframe to be a sublattice closed under the formation of arbitrary infs and directed sups. This notion corresponds with a subalgebra of a continuous lattice in [16].\par The class of completely distributive lattices is also introduced in the paper. Such lattices are complete and satisfy the most restrictive type of the general distributivity law. Obviously each completely distributive lattice is a Heyting algebra. It was hard to find the best Mizar implementation of the complete distributivity equational condition (denoted by CD in [16]). The powerful and well developed Many Sorted Theory gives the most convenient way of this formalization. A set double indexed by $K$, introduced in the paper, corresponds with a family $\{x_{j,k}: j\in J, k\in K(j)\}$. It is defined to be a suitable many sorted function. Two special functors: $\rm Sups$ and $\rm Infs$ as counterparts of $\rm Sup$ and $\rm Inf$ respectively, introduced in [33], are also defined. Originally the equation in Definition~2.4 of [16, p. 58] looks as follows: $${\textstyle\bigwedge}_{j\in J} {\textstyle\bigvee}_{k\in K(j)} x_{j,k} = {\textstyle\bigvee}_{f\in M} {\textstyle\bigwedge}_{j\in J} x_{j,f(j)},$$ where $M$ is the set of functions defined on $J$ with values $f(j)\in K(j)$.

This work was partially supported by the Office of Naval Research Grant N00014-95-1-1336.

MML Identifier: WAYBEL_5

Contents (PDF format)

1. The Continuity of Lattices
2. Completely-Distributive Lattices
3. Sub--Frames of Continuous Lattices

Acknowledgments

Bibliography

[1] Grzegorz Bancerek. Curried and uncurried functions. Journal of Formalized Mathematics, 2, 1990.

[2] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[3] Grzegorz Bancerek. Cartesian product of functions. Journal of Formalized Mathematics, 3, 1991.

[4] Grzegorz Bancerek. Complete lattices. Journal of Formalized Mathematics, 4, 1992.

[5] Grzegorz Bancerek. Bounds in posets and relational substructures. Journal of Formalized Mathematics, 8, 1996.

[6] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Journal of Formalized Mathematics, 8, 1996.

[7] Grzegorz Bancerek. The ``way-below'' relation. Journal of Formalized Mathematics, 8, 1996.

[8] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[10] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[11] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[12] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[13] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[14] Czeslaw Bylinski. Galois connections. Journal of Formalized Mathematics, 8, 1996.

[15] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[16] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. \em A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

[17] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Journal of Formalized Mathematics, 8, 1996.

[18] Peter T. Johnstone. \em Stone Spaces. Cambridge University Press, Cambridge, London, New York, 1982.

[19] Malgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[20] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.

[21] Beata Madras. Products of many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[22] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.

[23] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.

[24] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.

[25] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[26] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.

[27] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[28] Andrzej Trybulec. Moore-Smith convergence. Journal of Formalized Mathematics, 8, 1996.

[29] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.

[30] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.

[31] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[32] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[33] Mariusz Zynel and Czeslaw Bylinski. Properties of relational structures, posets, lattices and maps. Journal of Formalized Mathematics, 8, 1996.