Topological Manifolds

Karol Pąk

Formalized Mathematics (2014)

  • Volume: 22, Issue: 2, page 179-186
  • ISSN: 1426-2630

Abstract

top
Let us recall that a topological space M is a topological manifold if M is second-countable Hausdorff and locally Euclidean, i.e. each point has a neighborhood that is homeomorphic to an open ball of E n for some n. However, if we would like to consider a topological manifold with a boundary, we have to extend this definition. Therefore, we introduce here the concept of a locally Euclidean space that covers both cases (with and without a boundary), i.e. where each point has a neighborhood that is homeomorphic to a closed ball of En for some n. Our purpose is to prove, using the Mizar formalism, a number of properties of such locally Euclidean spaces and use them to demonstrate basic properties of a manifold. Let T be a locally Euclidean space. We prove that every interior point of T has a neighborhood homeomorphic to an open ball and that every boundary point of T has a neighborhood homeomorphic to a closed ball, where additionally this point is transformed into a point of the boundary of this ball. When T is n-dimensional, i.e. each point of T has a neighborhood that is homeomorphic to a closed ball of En, we show that the interior of T is a locally Euclidean space without boundary of dimension n and the boundary of T is a locally Euclidean space without boundary of dimension n − 1. Additionally, we show that every connected component of a compact locally Euclidean space is a locally Euclidean space of some dimension. We prove also that the Cartesian product of locally Euclidean spaces also forms a locally Euclidean space. We determine the interior and boundary of this product and show that its dimension is the sum of the dimensions of its factors. At the end, we present several consequences of these results for topological manifolds. This article is based on [14].

How to cite

top

Karol Pąk. "Topological Manifolds." Formalized Mathematics 22.2 (2014): 179-186. <http://eudml.org/doc/268877>.

@article{KarolPąk2014,
abstract = {Let us recall that a topological space M is a topological manifold if M is second-countable Hausdorff and locally Euclidean, i.e. each point has a neighborhood that is homeomorphic to an open ball of E n for some n. However, if we would like to consider a topological manifold with a boundary, we have to extend this definition. Therefore, we introduce here the concept of a locally Euclidean space that covers both cases (with and without a boundary), i.e. where each point has a neighborhood that is homeomorphic to a closed ball of En for some n. Our purpose is to prove, using the Mizar formalism, a number of properties of such locally Euclidean spaces and use them to demonstrate basic properties of a manifold. Let T be a locally Euclidean space. We prove that every interior point of T has a neighborhood homeomorphic to an open ball and that every boundary point of T has a neighborhood homeomorphic to a closed ball, where additionally this point is transformed into a point of the boundary of this ball. When T is n-dimensional, i.e. each point of T has a neighborhood that is homeomorphic to a closed ball of En, we show that the interior of T is a locally Euclidean space without boundary of dimension n and the boundary of T is a locally Euclidean space without boundary of dimension n − 1. Additionally, we show that every connected component of a compact locally Euclidean space is a locally Euclidean space of some dimension. We prove also that the Cartesian product of locally Euclidean spaces also forms a locally Euclidean space. We determine the interior and boundary of this product and show that its dimension is the sum of the dimensions of its factors. At the end, we present several consequences of these results for topological manifolds. This article is based on [14].},
author = {Karol Pąk},
journal = {Formalized Mathematics},
keywords = {locally Euclidean spaces; interior; boundary; Cartesian product},
language = {eng},
number = {2},
pages = {179-186},
title = {Topological Manifolds},
url = {http://eudml.org/doc/268877},
volume = {22},
year = {2014},
}

TY - JOUR
AU - Karol Pąk
TI - Topological Manifolds
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 2
SP - 179
EP - 186
AB - Let us recall that a topological space M is a topological manifold if M is second-countable Hausdorff and locally Euclidean, i.e. each point has a neighborhood that is homeomorphic to an open ball of E n for some n. However, if we would like to consider a topological manifold with a boundary, we have to extend this definition. Therefore, we introduce here the concept of a locally Euclidean space that covers both cases (with and without a boundary), i.e. where each point has a neighborhood that is homeomorphic to a closed ball of En for some n. Our purpose is to prove, using the Mizar formalism, a number of properties of such locally Euclidean spaces and use them to demonstrate basic properties of a manifold. Let T be a locally Euclidean space. We prove that every interior point of T has a neighborhood homeomorphic to an open ball and that every boundary point of T has a neighborhood homeomorphic to a closed ball, where additionally this point is transformed into a point of the boundary of this ball. When T is n-dimensional, i.e. each point of T has a neighborhood that is homeomorphic to a closed ball of En, we show that the interior of T is a locally Euclidean space without boundary of dimension n and the boundary of T is a locally Euclidean space without boundary of dimension n − 1. Additionally, we show that every connected component of a compact locally Euclidean space is a locally Euclidean space of some dimension. We prove also that the Cartesian product of locally Euclidean spaces also forms a locally Euclidean space. We determine the interior and boundary of this product and show that its dimension is the sum of the dimensions of its factors. At the end, we present several consequences of these results for topological manifolds. This article is based on [14].
LA - eng
KW - locally Euclidean spaces; interior; boundary; Cartesian product
UR - http://eudml.org/doc/268877
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. 
  2. [2] Grzegorz Bancerek. Tarski’s classes and ranks. Formalized Mathematics, 1(3):563–567, 1990. 
  3. [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. Zbl06213858
  4. [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  5. [5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. 
  6. [6] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990. 
  7. [7] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. 
  8. [8] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. 
  9. [9] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  10. [10] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990. 
  11. [11] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991. 
  12. [12] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  13. [13] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990. 
  14. [14] Ryszard Engelking. Teoria wymiaru. PWN, 1981. 
  15. [15] Adam Grabowski. Properties of the product of compact topological spaces. Formalized Mathematics, 8(1):55–59, 1999. 
  16. [16] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Formalized Mathematics, 2(5):665–674, 1991. 
  17. [17] Artur Korniłowicz. Jordan curve theorem. Formalized Mathematics, 13(4):481–491, 2005. 
  18. [18] Artur Korniłowicz. The definition and basic properties of topological groups. Formalized Mathematics, 7(2):217–225, 1998. 
  19. [19] Artur Korniłowicz and Yasunari Shidama. Brouwer fixed point theorem for disks on the plane. Formalized Mathematics, 13(2):333–336, 2005. 
  20. [20] Artur Korniłowicz and Yasunari Shidama. Intersections of intervals and balls in E n T. Formalized Mathematics, 12(3):301–306, 2004. 
  21. [21] Robert Milewski. Bases of continuous lattices. Formalized Mathematics, 7(2):285–294, 1998. 
  22. [22] Yatsuka Nakamura and Andrzej Trybulec. Components and unions of components. Formalized Mathematics, 5(4):513–517, 1996. 
  23. [23] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990. 
  24. [24] Beata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96, 1991. 
  25. [25] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990. 
  26. [26] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990. 
  27. [27] Karol Pąk. Tietze extension theorem for n-dimensional spaces. Formalized Mathematics, 22(1):11–19. doi:10.2478/forma-2014-0002.[Crossref] Zbl1298.54003
  28. [28] Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441–444, 1990. 
  29. [29] Marco Riccardi. The definition of topological manifolds. Formalized Mathematics, 19(1): 41–44, 2011. doi:10.2478/v10037-011-0007-4.[Crossref] Zbl1276.57023
  30. [30] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535–545, 1991. 
  31. [31] Andrzej Trybulec. On the geometry of a Go-Board. Formalized Mathematics, 5(3):347– 352, 1996. 
  32. [32] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  33. [33] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990. 
  34. [34] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.