:: The Definition of Topological Manifolds
:: by Marco Riccardi
::
:: Received August 17, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users

registration

let x, y be set ;

cluster {[x,y]} -> one-to-one ;

correctness
coherence
{[x,y]} is one-to-one ;

proof end;

end;

theorem :: MFOLD_1:1

canceled;

::$CT

theorem Th2: :: MFOLD_1:2

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

proof end;

definition

let n be Nat;
let S be Subset of (TOP-REAL n);

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

end;

:: deftheorem Def1 defines ball MFOLD_1:def 1 :
for n being Nat
for S being Subset of (TOP-REAL n) holds
( S is ball iff ex p being Point of (TOP-REAL n) ex r being Real st S = Ball (p,r) );

registration

let n be Nat;

cluster functional ball for Element of bool the carrier of (TOP-REAL n);

correctness
existence
ex b₁ being Subset of (TOP-REAL n) st b₁ is ball ;

proof end;

cluster ball -> open for Element of bool the carrier of (TOP-REAL n);

correctness
coherence
for b₁ being Subset of (TOP-REAL n) st b₁ is ball holds
b₁ is open ;
;

end;

registration

let n be Nat;

cluster non empty functional ball for Element of bool the carrier of (TOP-REAL n);

correctness
existence
ex b₁ being Subset of (TOP-REAL n) st
( not b₁ is empty & b₁ is ball );

proof end;

end;

theorem Th3: :: MFOLD_1:3

for n being Nat
for p being Point of (TOP-REAL n)
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 )

proof end;

definition

end;

:: deftheorem MFOLD_1:def 2 :
canceled;

definition

let n be Nat;

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

correctness
coherence
Tball ((0. (TOP-REAL n)),1) is SubSpace of TOP-REAL n;
;

end;

:: deftheorem defines Tunit_ball MFOLD_1:def 3 :
for n being Nat holds Tunit_ball n = Tball ((0. (TOP-REAL n)),1);

registration

let n be Nat;

cluster Tunit_ball n -> non empty ;

correctness
coherence
not Tunit_ball n is empty ;
;

end;

theorem :: MFOLD_1:4

canceled;

::$CT

theorem Th5: :: MFOLD_1:5

for n being Nat
for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds
|.p.| < 1

proof end;

theorem Th6: :: MFOLD_1:6

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

proof end;

:: like TOPREALB:19

theorem :: MFOLD_1:7

for n being Nat
for p being Point of (TOP-REAL n)
for r being positive Real
for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism

proof end;

theorem Th8: :: MFOLD_1:8

for n being Nat holds Tunit_ball n, TOP-REAL n are_homeomorphic

proof end;

theorem :: MFOLD_1:9

canceled;

::$CT

theorem Th10: :: MFOLD_1:10

for n being Nat
for B being non empty ball Subset of (TOP-REAL n) holds B, [#] (TOP-REAL n) are_homeomorphic

proof end;

theorem Th11: :: MFOLD_1:11

for M, N being non empty TopSpace
for p being Point of M
for U being a_neighborhood of p
for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )

proof end;

Lm1: for n being Nat
for M being non empty TopSpace st ( for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ) holds
for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

proof end;

theorem Def4: :: MFOLD_1:12

for n being Nat
for M being non empty TopSpace holds
( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic )

proof end;

registration

let n be Nat;

cluster TOP-REAL n -> n -locally_euclidean without_boundary ;

coherence
( TOP-REAL n is without_boundary & TOP-REAL n is n -locally_euclidean )

proof end;

end;

:: Lemma 2.13a

theorem :: MFOLD_1:13

for n being Nat
for M being non empty TopSpace holds
( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )

proof end;

:: Lemma 2.13b

theorem Th13: :: MFOLD_1:14

for n being Nat
for M being non empty TopSpace holds
( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )

proof end;

registration

cluster non empty TopSpace-like locally_euclidean without_boundary -> non empty first-countable for TopStruct ;

correctness
coherence
for b₁ being non empty TopSpace st b₁ is without_boundary & b₁ is locally_euclidean holds
b₁ is first-countable ;

proof end;

end;

set T = (TOP-REAL 0) | ([#] (TOP-REAL 0));

Lm2: (TOP-REAL 0) | ([#] (TOP-REAL 0)) = TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #)
by TSEP_1:93;

registration

cluster non empty TopSpace-like 0 -locally_euclidean -> non empty discrete for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is 0 -locally_euclidean holds
b₁ is discrete

proof end;

cluster non empty TopSpace-like discrete -> non empty 0 -locally_euclidean for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is discrete holds
b₁ is 0 -locally_euclidean

proof end;

end;

definition

let n be Nat;
let M be non empty TopSpace;

attr M is n -manifold means :: MFOLD_1:def 4
( M is second-countable & M is Hausdorff & M is n -locally_euclidean );

end;

:: deftheorem defines -manifold MFOLD_1:def 4 :
for n being Nat
for M being non empty TopSpace holds
( M is n -manifold iff ( M is second-countable & M is Hausdorff & M is n -locally_euclidean ) );

registration

let n be Nat;

cluster non empty TopSpace-like without_boundary n -manifold for TopStruct ;

existence
ex b₁ being non empty TopSpace st
( b₁ is without_boundary & b₁ is n -manifold )

proof end;

end;

registration

cluster non empty TopSpace-like second-countable discrete -> non empty Hausdorff second-countable 0 -locally_euclidean for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is second-countable & b₁ is discrete holds
( b₁ is 0 -locally_euclidean & b₁ is second-countable & b₁ is Hausdorff ) ;

end;

registration

let n be Nat;

cluster non empty TopSpace-like n -manifold -> non empty Hausdorff second-countable n -locally_euclidean for TopStruct ;

correctness
coherence
for b₁ being non empty TopSpace st b₁ is n -manifold holds
( b₁ is second-countable & b₁ is Hausdorff & b₁ is n -locally_euclidean );
;

cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean -> non empty n -manifold for TopStruct ;

correctness
coherence
for b₁ being non empty TopSpace st b₁ is second-countable & b₁ is Hausdorff & b₁ is n -locally_euclidean holds
b₁ is n -manifold ;
;

end;

:: Lemma 2.16

registration

let n be Nat;
let M be non empty without_boundary n -manifold TopSpace;

cluster non empty open -> non empty without_boundary n -manifold for SubSpace of M;

correctness
coherence
for b₁ being non empty SubSpace of M st b₁ is open holds
( b₁ is without_boundary & b₁ is n -manifold );

proof end;

end;