:: The Definition of Topological Manifolds
::  by Marco Riccardi
::
:: Received August 17, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, PRE_TOPC, EUCLID, ARYTM_1,
      ARYTM_3, SUPINF_2, XBOOLE_0, FUNCOP_1, ORDINAL2, TOPS_1, RCOMP_1,
      XXREAL_0, METRIC_1, TARSKI, STRUCT_0, REAL_1, COMPLEX1, SETFAM_1,
      PCOMPS_1, TOPS_2, T_0TOPSP, CONNSP_2, FUNCT_1, RELAT_1, CARD_1, SQUARE_1,
      TOPMETR, MEMBERED, XXREAL_1, XXREAL_2, WAYBEL23, COMPTS_1, RLVECT_3,
      NATTRA_1, ZFMISC_1, FRECHET, CARD_3, MFOLD_0, MFOLD_1, FUNCT_2, NAT_1,
      XCMPLX_0, BROUWER;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, TOPS_2, RELAT_1,
      RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0,
      COMPLEX1, STRUCT_0, PRE_TOPC, METRIC_1, TOPREAL9, TOPS_1, RLVECT_1,
      BORSUK_3, CONNSP_2, TSEP_1, METRIZTS, PCOMPS_1, COMPTS_1, EUCLID,
      SQUARE_1, TOPMETR, TMAP_1, XXREAL_1, MEMBERED, XXREAL_2, WAYBEL23,
      CANTOR_1, CARD_1, TDLAT_3, ZFMISC_1, CARD_3, YELLOW_8, FRECHET, BROUWER,
      MFOLD_0;
 constructors TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, TOPS_1, BORSUK_3,
      METRIZTS, COMPLEX1, BINOP_2, TMAP_1, WAYBEL23, CANTOR_1, TDLAT_3,
      YELLOW_8, FRECHET, SEQ_4, NUMBERS, BROUWER, MFOLD_0;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, MEMBERED,
      STRUCT_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TOPS_1,
      CARD_1, TSEP_1, TOPREAL9, COMPLEX1, TMAP_1, TOPMETR, XXREAL_2, TOPREAL1,
      YELLOW13, KURATO_2, SUBSET_1, RELSET_1, FUNCT_2, SQUARE_1, MFOLD_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Preliminaries

registration
  let x, y be set;
  cluster {[x,y]} -> one-to-one;
end;

reserve n for Nat;

::$CT

theorem :: MFOLD_1:2
  for X being non empty SubSpace of TOP-REAL n, f being Function of X,R^1
  st f is continuous
  ex g being Function of X,TOP-REAL n st
  (for a being Point of X, b being Point of TOP-REAL n, r being Real
  st a = b & f.a = r holds g.b = r*b) & g is continuous;

definition
  let n;
  let S be Subset of TOP-REAL n;
  attr S is ball means
:: MFOLD_1:def 1
  ex p being Point of TOP-REAL n, r being Real st S = Ball(p,r);
end;

registration
  let n;
  cluster ball for Subset of TOP-REAL n;
  cluster ball -> open for Subset of TOP-REAL n;
end;

registration
  let n;
  cluster non empty ball for Subset of TOP-REAL n;
end;

reserve p for Point of TOP-REAL n, r for Real;

theorem :: MFOLD_1:3
  for S being open Subset of TOP-REAL n st p in S holds
  ex B being ball Subset of TOP-REAL n st B c= S & p in B;

definition
::$CD
end;

definition
  let n;
  func Tunit_ball(n) -> SubSpace of TOP-REAL n equals
:: MFOLD_1:def 3
  Tball(0.(TOP-REAL n),1);
end;

registration
  let n;
  cluster Tunit_ball(n) -> non empty;
end;

::$CT

theorem :: MFOLD_1:5
  n <> 0 & p is Point of Tunit_ball(n) implies |. p .| < 1;

theorem :: MFOLD_1:6
  for f being Function of Tunit_ball n, TOP-REAL n st n <> 0 &
  for a being Point of Tunit_ball n, b being Point of TOP-REAL n
      st a = b holds f.a = 1/(1-|.b.|*|.b.|)*b
  holds f is being_homeomorphism;

:: like TOPREALB:19
theorem :: MFOLD_1:7
  for r being positive Real,
      f being Function of Tunit_ball(n), Tball(p,r) st n <> 0
  & for a being Point of Tunit_ball(n), b being Point of TOP-REAL n
      st a = b holds f.a = r*b+p
  holds f is being_homeomorphism;

theorem :: MFOLD_1:8
  Tunit_ball n, TOP-REAL n are_homeomorphic;

reserve q for Point of TOP-REAL n;

::$CT

theorem :: MFOLD_1:10
  for B being non empty ball Subset of TOP-REAL n
  holds B, [#]TOP-REAL n are_homeomorphic;

theorem :: MFOLD_1:11
  for M, N being non empty TopSpace
  for p being Point of M, U being a_neighborhood of p, B being open Subset of N
  st U,B are_homeomorphic
  ex V being open Subset of M, S being open Subset of N
     st V c= U & p in V & V,S are_homeomorphic;

begin :: Manifold

reserve M for non empty TopSpace;

theorem :: MFOLD_1:12
  M is n-locally_euclidean without_boundary iff
    for p being Point of M holds
      ex U being a_neighborhood of p, S being open Subset of TOP-REAL n
    st U,S are_homeomorphic;

registration
  let n;
  cluster TOP-REAL n -> without_boundary n-locally_euclidean;
end;

:: Lemma 2.13a
theorem :: MFOLD_1:13
  M is without_boundary n-locally_euclidean iff
  for p being Point of M holds
  ex U being a_neighborhood of p, B being ball Subset of TOP-REAL n
    st U,B are_homeomorphic;

:: Lemma 2.13b
theorem :: MFOLD_1:14
  M is without_boundary n-locally_euclidean iff
  for p being Point of M holds
  ex U being a_neighborhood of p st U,[#]TOP-REAL n are_homeomorphic;

registration
  cluster without_boundary locally_euclidean ->
     first-countable for non empty TopSpace;
end;

registration
  cluster 0-locally_euclidean -> discrete for non empty TopSpace;
  cluster discrete -> 0-locally_euclidean for non empty TopSpace;
end;

definition
  let n, M;
  attr M is n-manifold means
:: MFOLD_1:def 4
     M is second-countable Hausdorff n-locally_euclidean;
end;

registration
  let n;
  cluster without_boundary n-manifold for non empty TopSpace;
end;

registration
  cluster second-countable discrete ->
     0-locally_euclidean second-countable Hausdorff
       for non empty TopSpace;
end;

registration
  let n;
  cluster n-manifold ->
          second-countable Hausdorff n-locally_euclidean for
             non empty TopSpace;
  cluster second-countable Hausdorff n-locally_euclidean ->
          n-manifold for non empty TopSpace;
end;

:: Lemma 2.16
registration
  let n;
  let M be without_boundary n-manifold non empty TopSpace;
  cluster open -> without_boundary n-manifold for non empty SubSpace of M;
end;