Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Connected Spaces

Beata Padlewska
Warsaw University, Bialystok
Supported by RPBP.III-24.C1.


The following notions are defined: separated sets, connected spaces, connected sets, components of a topological space, the component of a point. The definition of the boundary of a set is also included. The singleton of a point of a topological space is redefined as a subset of the space. Some theorems about these notions are proved.

MML Identifier: CONNSP_1

The terminology and notation used in this paper have been introduced in the following articles [3] [4] [1] [2] [5]

Contents (PDF format)


[1] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[2] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[3] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[4] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[5] Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.

Received May 6, 1989

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