On the Kuratowski Limit Operators

Adam Grabowski

University of Bialystok

Summary.

In the paper we give formal descriptions of the two Kuratowski limit oprators: Li $S$ and Ls $S$, where $S$ is an arbitrary sequence of subsets of a fixed topological space. In the two last sections we prove basic properties of these lower and upper topological limits, which may be found e.g. in [19]. In the sections 2-4, we present three operators which are associated in some sense with the above mentioned, that is lim inf $F$, lim sup $F$, and limes $F$, where $F$ is a sequence of subsets of a fixed 1-sorted structure.

This work has been partially supported by the CALCULEMUS grant HPRN-CT-2000-00102.

MML Identifier: KURATO_2

Contents (PDF format)

1. Preliminaries
2. Lower and Upper Limit of Sequences of Subsets
3. Ascending and Descending Families of Subsets
4. Constant and Convergent Sequences
5. Topological Lemmas
6. Subsequences
7. The Lower Topological Limit
8. The Upper Topological Limit

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

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

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[5] Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.

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

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

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

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

[10] Czeslaw Bylinski and Piotr Rudnicki. Bounding boxes for compact sets in $\calE^2$. Journal of Formalized Mathematics, 9, 1997.

[11] Czeslaw Bylinski and Mariusz Zynel. Cages - the external approximation of Jordan's curve. Journal of Formalized Mathematics, 11, 1999.

[12] Agata Darmochwal. Compact spaces. Journal of Formalized Mathematics, 1, 1989.

[13] Agata Darmochwal. The Euclidean space. Journal of Formalized Mathematics, 3, 1991.

[14] Agata Darmochwal and Yatsuka Nakamura. The topological space $\calE^2_\rmT$. Arcs, line segments and special polygonal arcs. Journal of Formalized Mathematics, 3, 1991.

[15] Agata Darmochwal and Yatsuka Nakamura. The topological space $\calE^2_\rmT$. Simple closed curves. Journal of Formalized Mathematics, 3, 1991.

[16] Stanislawa Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Journal of Formalized Mathematics, 2, 1990.

[17] Jaroslaw Kotowicz. Monotone real sequences. Subsequences. Journal of Formalized Mathematics, 1, 1989.

[18] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.

[19] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.

[20] Yatsuka Nakamura, Andrzej Trybulec, and Czeslaw Bylinski. Bounded domains and unbounded domains. Journal of Formalized Mathematics, 11, 1999.

[21] Andrzej Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.

[22] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.

[23] Beata Padlewska. Locally connected spaces. Journal of Formalized Mathematics, 2, 1990.

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

[25] Jan Popiolek. Real normed space. Journal of Formalized Mathematics, 2, 1990.

[26] Agnieszka Sakowicz, Jaroslaw Gryko, and Adam Grabowski. Sequences in $\calE^N_\rmT$. Journal of Formalized Mathematics, 6, 1994.

[27] Bartlomiej Skorulski. First-countable, sequential, and Frechet spaces. Journal of Formalized Mathematics, 10, 1998.

[28] Bartlomiej Skorulski. The sequential closure operator in sequential and Frechet spaces. Journal of Formalized Mathematics, 11, 1999.

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

[30] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.

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

[32] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

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

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

[35] Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.