@MISC{MFOLD_0.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Topological Manifolds},
  NOTE = {The paper has been financed by the
    resources of the Polish National Science Centre granted by decision
    no. DEC-2012/07/N/ST6/02147.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Locally Euclidean Spaces},
  SECTION3 = {Locally Euclidean Spaces With and Without a Boundary},
  SECTION4 = {Interior and Boundary of Locally Euclidean Spaces},
  SECTION5 = {Cartesian Product of Locally Euclidean Spaces},
  SECTION6 = {Fixed Dimension Locally Euclidean Spaces},
  SECTION7 = {Connected Components of Locally Euclidean Spaces},
  SECTION8 = {Topological Manifold},
  DAY = {16},
  MONTH = {June},
  YEAR = {2014},
  ADDRESS1 = {Institute of Computer Science\\University of Bia{\l}ystok\\Sosnowa 64, 15-887 Bia{\l}ystok\\Poland},
  SUMMARY = {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 ${\cal 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 ${\cal E}^n$ for some $n$.
  \par 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 ${\cal E}^n$, 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 \cite{ENGEL:BM51}.}}

