:: Topological Manifolds
:: by Karol P\kak
::
:: Received June 16, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


theorem Th1: :: MFOLD_0:1
for T being non empty TopSpace holds T,T | ([#] T) are_homeomorphic
proof end;

definition
let n be Nat;
let p be Point of (TOP-REAL n);
let r be Real;
func Tball (p,r) -> SubSpace of TOP-REAL n equals :: MFOLD_0:def 1
(TOP-REAL n) | (Ball (p,r));
correctness
coherence
(TOP-REAL n) | (Ball (p,r)) is SubSpace of TOP-REAL n;
;
end;

:: deftheorem defines Tball MFOLD_0:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for r being Real holds Tball (p,r) = (TOP-REAL n) | (Ball (p,r));

registration
let n be Nat;
let p be Point of (TOP-REAL n);
let s be positive Real;
cluster Tball (p,s) -> non empty ;
correctness
coherence
not Tball (p,s) is empty ;
;
end;

theorem :: MFOLD_0:2
for n being Nat
for p being Point of (TOP-REAL n)
for r being Real holds the carrier of (Tball (p,r)) = Ball (p,r)
proof end;

theorem Th3: :: MFOLD_0:3
for n being Nat
for p, q being Point of (TOP-REAL n)
for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic
proof end;

registration
let n be Nat;
cluster TOP-REAL n -> second-countable ;
correctness
coherence
TOP-REAL n is second-countable ;
proof end;
end;

Lm1: for n being Nat
for p, q being Point of (TOP-REAL n)
for r, s being real number st r > 0 & s > 0 holds
Tdisk (p,r), Tdisk (q,s) are_homeomorphic
proof end;

theorem :: MFOLD_0:4
for n being Nat
for M being non empty TopSpace
for q being Point of M
for r being real number
for p being Point of (TOP-REAL n) st r > 0 holds
for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
proof end;

definition
let M be non empty TopSpace;
attr M is locally_euclidean means :Def2: :: MFOLD_0:def 2
 for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ;
end;

:: deftheorem Def2 defines locally_euclidean MFOLD_0:def 2 :
for M being non empty TopSpace holds
( M is locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic );

definition
let n be Nat;
let M be non empty TopSpace;
attr M is n -locally_euclidean means :Def3: :: MFOLD_0:def 3
 for p being Point of M ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ;
end;

:: deftheorem Def3 defines -locally_euclidean MFOLD_0:def 3 :
for n being Nat
for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic );

registration
let n be Nat;
cluster Tdisk ((0. (TOP-REAL n)),1) -> n -locally_euclidean ;
coherence
Tdisk ((0. (TOP-REAL n)),1) is n -locally_euclidean
proof end;
end;

registration
let n be Nat;
cluster non empty TopSpace-like n -locally_euclidean for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is n -locally_euclidean
proof end;
end;

registration
let n be Nat;
cluster non empty TopSpace-like n -locally_euclidean -> non empty locally_euclidean for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is n -locally_euclidean holds
b1 is locally_euclidean
proof end;
end;

definition
let M be non empty TopSpace;
func Int M -> Subset of M means :Def4: :: MFOLD_0:def 4
 for p being Point of M holds
( p in it iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic );
existence
ex b1 being Subset of M st
for p being Point of M holds
( p in b1 iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
proof end;
uniqueness
for b1, b2 being Subset of M st ( for p being Point of M holds
( p in b1 iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ) & ( for p being Point of M holds
( p in b2 iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Int MFOLD_0:def 4 :
for M being non empty TopSpace
for b2 being Subset of M holds
( b2 = Int M iff for p being Point of M holds
( p in b2 iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) );

registration
let M be non empty locally_euclidean TopSpace;
cluster Int M -> non empty open ;
coherence
( not Int M is empty & Int M is open )
proof end;
end;

definition
let M be non empty TopSpace;
func Fr M -> Subset of M equals :: MFOLD_0:def 5
(Int M) ` ;
coherence
(Int M) ` is Subset of M ;
end;

:: deftheorem defines Fr MFOLD_0:def 5 :
for M being non empty TopSpace holds Fr M = (Int M) ` ;

:: WP: Boundary Points of Locally Euclidean Spaces
theorem Th5: :: MFOLD_0:5
for M being non empty locally_euclidean TopSpace
for p being Point of M holds
( p in Fr M iff ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
proof end;

definition
let M be non empty TopSpace;
attr M is without_boundary means :Def6: :: MFOLD_0:def 6
 Int M = the carrier of M;
end;

:: deftheorem Def6 defines without_boundary MFOLD_0:def 6 :
for M being non empty TopSpace holds
( M is without_boundary iff Int M = the carrier of M );

notation
let M be non empty TopSpace;
antonym with_boundary M for without_boundary ;
end;

Lm2: for M being non empty TopSpace holds
( ( M is locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
proof end;

Lm3: for n being Nat holds
( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & Tball ((0. (TOP-REAL n)),1) is without_boundary )
proof end;

registration
let n be Nat;
cluster Tball ((0. (TOP-REAL n)),1) -> n -locally_euclidean without_boundary ;
coherence
( Tball ((0. (TOP-REAL n)),1) is without_boundary & Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean ) by Lm3;
end;

registration
let n be non zero Nat;
cluster Tdisk ((0. (TOP-REAL n)),1) -> with_boundary ;
coherence
not Tdisk ((0. (TOP-REAL n)),1) is without_boundary
proof end;
end;

registration
let n be Nat;
cluster non empty TopSpace-like locally_euclidean n -locally_euclidean without_boundary for TopStruct ;
existence
ex b1 being non empty n -locally_euclidean TopSpace st b1 is without_boundary
proof end;
end;

registration
let n be non zero Nat;
cluster non empty TopSpace-like compact locally_euclidean n -locally_euclidean with_boundary for TopStruct ;
existence
ex b1 being non empty n -locally_euclidean TopSpace st
( b1 is with_boundary & b1 is compact )
proof end;
end;

registration
let M be non empty locally_euclidean without_boundary TopSpace;
cluster Fr M -> empty ;
coherence
Fr M is empty
proof end;
end;

registration
let M be non empty locally_euclidean with_boundary TopSpace;
cluster Fr M -> non empty ;
coherence
not Fr M is empty
proof end;
end;

registration
let n be zero Nat;
cluster non empty TopSpace-like n -locally_euclidean -> non empty n -locally_euclidean without_boundary for TopStruct ;
coherence
for b1 being non empty n -locally_euclidean TopSpace holds b1 is without_boundary
proof end;
end;

:: Correspondence between Classical and Extended Concepts
:: of Locally Euclidean Spaces
theorem :: MFOLD_0:6
for M being non empty TopSpace holds
( M is non empty locally_euclidean without_boundary TopSpace iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) by Lm2;

theorem Th7: :: MFOLD_0:7
for M being non empty locally_euclidean with_boundary TopSpace
for p being Point of M
for n being Nat st ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic holds
for pF being Point of (M | (Fr M)) st p = pF holds
ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
proof end;

Lm4: for M being non empty locally_euclidean TopSpace
for p being Point of (M | (Int M)) ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
proof end;

registration
let M be non empty locally_euclidean TopSpace;
cluster M | (Int M) -> locally_euclidean ;
coherence
M | (Int M) is locally_euclidean
proof end;
cluster M | (Int M) -> without_boundary ;
coherence
M | (Int M) is without_boundary
proof end;
end;

Lm5: for M being non empty locally_euclidean with_boundary TopSpace
for p being Point of M
for pM being Point of (M | (Fr M)) st p = pM holds
for U being a_neighborhood of p
for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
proof end;

registration
let M be non empty locally_euclidean with_boundary TopSpace;
cluster M | (Fr M) -> locally_euclidean ;
coherence
M | (Fr M) is locally_euclidean
proof end;
cluster M | (Fr M) -> without_boundary ;
coherence
M | (Fr M) is without_boundary
proof end;
end;

registration
let N, M be non empty locally_euclidean TopSpace;
cluster [:N,M:] -> locally_euclidean ;
coherence
[:N,M:] is locally_euclidean
proof end;
end;

theorem Th8: :: MFOLD_0:8
for N, M being non empty locally_euclidean TopSpace holds Int [:N,M:] = [:(Int N),(Int M):]
proof end;

theorem Th9: :: MFOLD_0:9
for N, M being non empty locally_euclidean TopSpace holds Fr [:N,M:] = [:([#] N),(Fr M):] \/ [:(Fr N),([#] M):]
proof end;

registration
let N, M be non empty locally_euclidean without_boundary TopSpace;
cluster [:N,M:] -> without_boundary ;
coherence
[:N,M:] is without_boundary
proof end;
end;

registration
let N be non empty locally_euclidean TopSpace;
let M be non empty locally_euclidean with_boundary TopSpace;
cluster [:N,M:] -> with_boundary ;
coherence
not [:N,M:] is without_boundary
proof end;
cluster [:M,N:] -> with_boundary ;
coherence
not [:M,N:] is without_boundary
proof end;
end;

definition
let n be Nat;
let M be non empty n -locally_euclidean TopSpace;
:: original: Int
redefine func Int M -> Subset of M means :Def7: :: MFOLD_0:def 7
 for p being Point of M holds
( p in it iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic );
compatibility
for b1 being Subset of M holds
( b1 = Int M iff for p being Point of M holds
( p in b1 iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) )
proof end;
coherence
Int M is Subset of M ;
end;

:: deftheorem Def7 defines Int MFOLD_0:def 7 :
for n being Nat
for M being non empty b1 -locally_euclidean TopSpace
for b3 being Subset of M holds
( b3 = Int M iff for p being Point of M holds
( p in b3 iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) );

definition
let n be Nat;
let M be non empty n -locally_euclidean TopSpace;
:: original: Fr
redefine func Fr M -> Subset of M means :: MFOLD_0:def 8
 for p being Point of M holds
( p in it iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) );
compatibility
for b1 being Subset of M holds
( b1 = Fr M iff for p being Point of M holds
( p in b1 iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) )
proof end;
coherence
Fr M is Subset of M ;
end;

:: deftheorem defines Fr MFOLD_0:def 8 :
for n being Nat
for M being non empty b1 -locally_euclidean TopSpace
for b3 being Subset of M holds
( b3 = Fr M iff for p being Point of M holds
( p in b3 iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) );

theorem :: MFOLD_0:10
for M1, M2 being non empty TopSpace st M1 is locally_euclidean & M1,M2 are_homeomorphic holds
M2 is locally_euclidean
proof end;

theorem Th11: :: MFOLD_0:11
for n being Nat
for M1, M2 being non empty TopSpace st M1 is n -locally_euclidean & M2 is locally_euclidean & M1,M2 are_homeomorphic holds
M2 is n -locally_euclidean
proof end;

:: WP: Topological Invariance of Dimension of Locally Euclidean Spaces
theorem :: MFOLD_0:12
for n, m being Nat
for M being non empty TopSpace st M is n -locally_euclidean & M is m -locally_euclidean holds
n = m
proof end;

theorem Th13: :: MFOLD_0:13
for n being Nat
for M being non empty TopSpace holds
( M is non empty b1 -locally_euclidean without_boundary TopSpace iff for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
proof end;

:: WP: Dimension of the Cartesian Product of Locally Euclidean Spaces
registration
let n, m be Element of NAT ;
let N be non empty n -locally_euclidean TopSpace;
let M be non empty m -locally_euclidean TopSpace;
cluster [:N,M:] -> n + m -locally_euclidean ;
coherence
[:N,M:] is n + m -locally_euclidean
proof end;
end;

:: WP: Dimension of the Interior of Locally Euclidean Spaces
registration
let n be Nat;
let M be non empty n -locally_euclidean TopSpace;
cluster M | (Int M) -> non empty n -locally_euclidean for non empty TopSpace;
coherence
for b1 being non empty TopSpace st b1 = M | (Int M) holds
b1 is n -locally_euclidean
proof end;
end;

:: WP: Dimension of the Boundary of Locally Euclidean Spaces
registration
let n be non zero Nat;
let M be non empty n -locally_euclidean with_boundary TopSpace;
cluster M | (Fr M) -> non empty n -' 1 -locally_euclidean for non empty TopSpace;
coherence
for b1 being non empty TopSpace st b1 = M | (Fr M) holds
b1 is n -' 1 -locally_euclidean
proof end;
end;

theorem Th14: :: MFOLD_0:14
for M being non empty compact locally_euclidean TopSpace
for C being Subset of M st C is a_component holds
( C is open & ex n being Nat st M | C is non empty b3 -locally_euclidean TopSpace )
proof end;

theorem :: MFOLD_0:15
for M being non empty compact locally_euclidean TopSpace ex P being a_partition of the carrier of M st
for A being Subset of M st A in P holds
( A is open & A is a_component & ex n being Nat st M | A is non empty b4 -locally_euclidean TopSpace )
proof end;

theorem :: MFOLD_0:16
for M being non empty compact locally_euclidean TopSpace st M is connected holds
ex n being Nat st M is n -locally_euclidean
proof end;

registration
let n be Nat;
cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean for TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean )
proof end;
end;

definition
mode topological_manifold is non empty Hausdorff second-countable locally_euclidean TopSpace;
end;

notation
let n be Nat;
let M be topological_manifold;
synonym n -dimensional M for n -locally_euclidean ;
end;

registration
let n be Nat;
cluster non empty TopSpace-like T_0 T_1 T_2 second-countable V413() locally_euclidean n -dimensional without_boundary for TopStruct ;
existence
ex b1 being topological_manifold st
( b1 is n -dimensional & b1 is without_boundary )
proof end;
end;

registration
let n be non zero Nat;
cluster non empty TopSpace-like T_0 T_1 T_2 compact second-countable V413() locally_euclidean n -dimensional with_boundary for TopStruct ;
existence
ex b1 being topological_manifold st
( b1 is n -dimensional & b1 is compact & b1 is with_boundary )
proof end;
end;

registration
let M be topological_manifold;
cluster non empty -> non empty Hausdorff second-countable for SubSpace of M;
coherence
for b1 being non empty SubSpace of M holds
( b1 is second-countable & b1 is Hausdorff )
proof end;
end;

registration
let M1, M2 be topological_manifold;
cluster [:M1,M2:] -> Hausdorff second-countable ;
coherence
( [:M1,M2:] is second-countable & [:M1,M2:] is T_2 ) ;
end;