Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

Continuous Lattices of Maps between T$_0$ Spaces


Grzegorz Bancerek
University of Bialystok

Summary.

Formalization of [20, pp. 128-130], chapter II, section 4 (4.1 - 4.9).

This work has been supported by KBN Grant 8 T11C 018 12.

MML Identifier: WAYBEL26

The terminology and notation used in this paper have been introduced in the following articles [32] [15] [38] [33] [19] [39] [13] [40] [18] [12] [16] [1] [10] [30] [2] [35] [27] [28] [29] [37] [3] [14] [31] [24] [11] [42] [34] [4] [5] [6] [22] [41] [17] [8] [7] [25] [36] [23] [21] [26] [9]

Contents (PDF format)

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. Complete lattices. Journal of Formalized Mathematics, 4, 1992.
[4] Grzegorz Bancerek. Quantales. Journal of Formalized Mathematics, 6, 1994.
[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] Grzegorz Bancerek. Bases and refinements of topologies. Journal of Formalized Mathematics, 10, 1998.
[9] Grzegorz Bancerek. Retracts and inheritance. Journal of Formalized Mathematics, 11, 1999.
[10] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.
[11] Jozef Bialas and Yatsuka Nakamura. Dyadic numbers and T$_4$ topological spaces. Journal of Formalized Mathematics, 7, 1995.
[12] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[13] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[14] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[15] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[16] 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.
[17] Czeslaw Bylinski. Galois connections. Journal of Formalized Mathematics, 8, 1996.
[18] Agata Darmochwal. Families of subsets, subspaces and mappings in topological spaces. Journal of Formalized Mathematics, 1, 1989.
[19] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[20] 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.
[21] Adam Grabowski. Scott-continuous functions. Part II. Journal of Formalized Mathematics, 11, 1999.
[22] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Journal of Formalized Mathematics, 8, 1996.
[23] Jaroslaw Gryko. Injective spaces. Journal of Formalized Mathematics, 10, 1998.
[24] Zbigniew Karno. On Kolmogorov topological spaces. Journal of Formalized Mathematics, 6, 1994.
[25] Artur Kornilowicz. On the topological properties of meet-continuous lattices. Journal of Formalized Mathematics, 8, 1996.
[26] Artur Kornilowicz and Jaroslaw Gryko. Injective spaces. Part II. Journal of Formalized Mathematics, 11, 1999.
[27] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.
[28] Beata Madras. Products of many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[29] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.
[30] Andrzej Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.
[31] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[32] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[33] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[34] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
[35] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[36] Andrzej Trybulec. Scott topology. Journal of Formalized Mathematics, 9, 1997.
[37] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[38] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[39] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[40] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.
[41] Mariusz Zynel and Czeslaw Bylinski. Properties of relational structures, posets, lattices and maps. Journal of Formalized Mathematics, 8, 1996.
[42] Mariusz Zynel and Adam Guzowski. \Tzero\ topological spaces. Journal of Formalized Mathematics, 6, 1994.

Received September 24, 1999

[ Download a postscript version, MML identifier index, Mizar home page]