<abstract xmlns="http://www.w3.org/1999/xhtml">Let us recall that a topological space <italic>M</italic> is a topological manifold if <italic>M</italic> is second-countable Hausdorff and locally Euclidean, i.e. each point has a neighborhood that is homeomorphic to an open ball of <italic>E</italic><italic>n</italic> for some <italic>n</italic>. 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 <italic>En</italic> for some <italic>n</italic>.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 <italic>T</italic> be a locally Euclidean space. We prove that every interior point of <italic>T</italic> has a neighborhood homeomorphic to an open ball and that every boundary point of <italic>T</italic> has a neighborhood homeomorphic to a closed ball, where additionally this point is transformed into a point of the boundary of this ball. When <italic>T</italic> is <italic>n-dimensional</italic>, i.e. each point of <italic>T</italic> has a neighborhood that is homeomorphic to a closed ball of <italic>En</italic>, we show that the interior of <italic>T</italic> is a locally Euclidean space without boundary of dimension <italic>n</italic> and the boundary of <italic>T</italic> is a locally Euclidean space without boundary of dimension <italic>n −</italic> 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].</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 En 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].

Topological Manifolds

Institute of Informatics University of Białystok Sosnowa 64, 15-887 Białystok Poland

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"Topological Manifolds"}

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...

Topological Manifolds

Published Online: Jun 30, 2014

Page range: 179 - 186

Received: Jun 16, 2014

DOI: https://doi.org/10.2478/forma-2014-0019

Keywords
locally Euclidean spaces, interior, boundary, Cartesian product

© 2014 Karol Pąk

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Topological Manifolds

Published Online: Jun 30, 2014

Page range: 179 - 186

Received: Jun 16, 2014

DOI: https://doi.org/10.2478/forma-2014-0019

Keywordslocally Euclidean spaces, interior, boundary, Cartesian product

© 2014 Karol Pąk

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Keywords
locally Euclidean spaces, interior, boundary, Cartesian product