Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

**Andrzej Trybulec**- Warsaw University, Bialystok

- We present a Borsuk's theorem published first in [1] (compare also [2, pages 119-120]). It is slightly generalized, the assumption of the metrizability is omitted. We introduce concepts needed for the formulation and the proofs of the theorems on upper semi-continuous decompositions, retracts, strong deformation retract. However, only those facts that are necessary in the proof have been proved.

- Preliminaries
- Partitions
- Topological Preliminaries
- Cartesian Product of Topological Spaces
- Partitions of Topological Spaces
- Upper Semicontinuous Decompositions
- Borsuk's Theorems on the Decomposition of Retracts

- [1] Karol Borsuk. On the homotopy types of some decomposition spaces. \em Bull. Acad. Polon. Sci., (18):235--239, 1970.
- [2] Karol Borsuk. \em Theory of Shape, volume 59 of \em Monografie Matematyczne. PWN, Warsaw, 1975.
- [3]
Leszek Borys.
Paracompact and metrizable spaces.
*Journal of Formalized Mathematics*, 3, 1991. - [4]
Czeslaw Bylinski.
Basic functions and operations on functions.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Czeslaw Bylinski.
Partial functions.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [9]
Agata Darmochwal.
Compact spaces.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Agata Darmochwal.
Families of subsets, subspaces and mappings in topological spaces.
*Journal of Formalized Mathematics*, 1, 1989. - [11]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Stanislawa Kanas, Adam Lecko, and Mariusz Startek.
Metric spaces.
*Journal of Formalized Mathematics*, 2, 1990. - [13]
Beata Padlewska.
Families of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [14]
Beata Padlewska.
Locally connected spaces.
*Journal of Formalized Mathematics*, 2, 1990. - [15]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Konrad Raczkowski and Pawel Sadowski.
Equivalence relations and classes of abstraction.
*Journal of Formalized Mathematics*, 1, 1989. - [17]
Konrad Raczkowski and Pawel Sadowski.
Topological properties of subsets in real numbers.
*Journal of Formalized Mathematics*, 2, 1990. - [18]
Andrzej Trybulec.
Binary operations applied to functions.
*Journal of Formalized Mathematics*, 1, 1989. - [19]
Andrzej Trybulec.
Domains and their Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [20]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [21]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [22]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [23]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [24]
Miroslaw Wysocki and Agata Darmochwal.
Subsets of topological spaces.
*Journal of Formalized Mathematics*, 1, 1989.

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