:: by Karol P\kak

::

:: Received June 16, 2014

:: Copyright (c) 2014-2019 Association of Mizar Users

definition

let n be Nat;

let p be Point of (TOP-REAL n);

let r be Real;

correctness

coherence

(TOP-REAL n) | (Ball (p,r)) is SubSpace of TOP-REAL n;

;

end;
let p be Point of (TOP-REAL n);

let r be Real;

correctness

coherence

(TOP-REAL n) | (Ball (p,r)) is SubSpace of TOP-REAL n;

;

:: 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));

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;

correctness

coherence

not Tball (p,s) is empty ;

;

end;
let p be Point of (TOP-REAL n);

let s be positive Real;

correctness

coherence

not Tball (p,s) is empty ;

;

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)

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

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;

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 )

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;

end;
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 ;

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 ;

:: 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 );

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;

end;
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 ;

for p being Point of M ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ;

:: 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 );

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
end;

registration

let n be Nat;

existence

ex b_{1} being non empty TopSpace st b_{1} is n -locally_euclidean

end;
existence

ex b

proof end;

registration

let n be Nat;

coherence

for b_{1} being non empty TopSpace st b_{1} is n -locally_euclidean holds

b_{1} is locally_euclidean

end;
coherence

for b

b

proof end;

definition

let M be non empty TopSpace;

ex b_{1} being Subset of M st

for p being Point of M holds

( p in b_{1} iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )

for b_{1}, b_{2} being Subset of M st ( for p being Point of M holds

( p in b_{1} 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 b_{2} iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ) holds

b_{1} = b_{2}

end;
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 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 );

ex b

for p being Point of M holds

( p in b

proof end;

uniqueness for b

( p in b

( p in b

b

proof end;

:: deftheorem Def4 defines Int MFOLD_0:def 4 :

for M being non empty TopSpace

for b_{2} being Subset of M holds

( b_{2} = Int M iff for p being Point of M holds

( p in b_{2} iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) );

for M being non empty TopSpace

for b

( b

( p in b

registration

let M be non empty locally_euclidean TopSpace;

coherence

( not Int M is empty & Int M is open )

end;
coherence

( not Int M is empty & Int M is open )

proof end;

:: 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) ) )

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;

:: 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 );

for M being non empty TopSpace holds

( M is without_boundary iff Int M = the carrier of M );

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;

coherence

( Tball ((0. (TOP-REAL n)),1) is without_boundary & Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean ) by Lm3;

end;
coherence

( Tball ((0. (TOP-REAL n)),1) is without_boundary & Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean ) by Lm3;

registration
end;

registration

let n be Nat;

ex b_{1} being non empty n -locally_euclidean TopSpace st b_{1} is without_boundary

end;
cluster non empty TopSpace-like locally_euclidean n -locally_euclidean without_boundary for TopStruct ;

existence ex b

proof end;

registration

let n be non zero Nat;

ex b_{1} being non empty n -locally_euclidean TopSpace st

( b_{1} is with_boundary & b_{1} is compact )

end;
cluster non empty TopSpace-like compact locally_euclidean n -locally_euclidean with_boundary for TopStruct ;

existence ex b

( b

proof end;

registration
end;

registration
end;

registration

let n be zero Nat;

for b_{1} being non empty n -locally_euclidean TopSpace holds b_{1} is without_boundary

end;
cluster non empty TopSpace-like n -locally_euclidean -> non empty n -locally_euclidean without_boundary for TopStruct ;

coherence for b

proof end;

:: Correspondence between Classical and Extended Concepts

:: of Locally Euclidean Spaces

:: 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 )

( 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 )

proof end;

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

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;

coherence

M | (Int M) is locally_euclidean

M | (Int M) is without_boundary

end;
coherence

M | (Int M) is locally_euclidean

proof end;

coherence M | (Int M) is without_boundary

proof 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;

coherence

M | (Fr M) is locally_euclidean

M | (Fr M) is without_boundary

end;
coherence

M | (Fr M) is locally_euclidean

proof end;

coherence M | (Fr M) is without_boundary

proof end;

registration
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;

coherence

[:N,M:] is without_boundary

end;
coherence

[:N,M:] is without_boundary

proof end;

registration

let N be non empty locally_euclidean TopSpace;

let M be non empty locally_euclidean with_boundary TopSpace;

coherence

not [:N,M:] is without_boundary

not [:M,N:] is without_boundary

end;
let M be non empty locally_euclidean with_boundary TopSpace;

coherence

not [:N,M:] is without_boundary

proof end;

coherence not [:M,N:] is without_boundary

proof end;

definition

let n be Nat;

let M be non empty n -locally_euclidean TopSpace;

for b_{1} being Subset of M holds

( b_{1} = Int M iff for p being Point of M holds

( p in b_{1} iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) )

Int M is Subset of M ;

end;
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 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 );

for b

( b

( p in b

proof end;

coherence Int M is Subset of M ;

:: deftheorem Def7 defines Int MFOLD_0:def 7 :

for n being Nat

for M being non empty b_{1} -locally_euclidean TopSpace

for b_{3} being Subset of M holds

( b_{3} = Int M iff for p being Point of M holds

( p in b_{3} iff ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) );

for n being Nat

for M being non empty b

for b

( b

( p in b

definition

let n be Nat;

let M be non empty n -locally_euclidean TopSpace;

for b_{1} being Subset of M holds

( b_{1} = Fr M iff for p being Point of M holds

( p in b_{1} 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) ) ) )

Fr M is Subset of M ;

end;
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 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) ) );

for b

( b

( p in b

( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) )

proof end;

coherence Fr M is Subset of M ;

:: deftheorem defines Fr MFOLD_0:def 8 :

for n being Nat

for M being non empty b_{1} -locally_euclidean TopSpace

for b_{3} being Subset of M holds

( b_{3} = Fr M iff for p being Point of M holds

( p in b_{3} 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) ) ) );

for n being Nat

for M being non empty b

for b

( b

( p in b

( 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

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

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;

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

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 b_{1} -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 )

for M being non empty TopSpace holds

( M is non empty b

proof end;

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;

coherence

[:N,M:] is n + m -locally_euclidean

end;
let N be non empty n -locally_euclidean TopSpace;

let M be non empty m -locally_euclidean TopSpace;

coherence

[:N,M:] is n + m -locally_euclidean

proof end;

registration

let n be Nat;

let M be non empty n -locally_euclidean TopSpace;

coherence

for b_{1} being non empty TopSpace st b_{1} = M | (Int M) holds

b_{1} is n -locally_euclidean

end;
let M be non empty n -locally_euclidean TopSpace;

coherence

for b

b

proof end;

registration

let n be non zero Nat;

let M be non empty n -locally_euclidean with_boundary TopSpace;

coherence

for b_{1} being non empty TopSpace st b_{1} = M | (Fr M) holds

b_{1} is n -' 1 -locally_euclidean

end;
let M be non empty n -locally_euclidean with_boundary TopSpace;

coherence

for b

b

proof 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 b_{3} -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 b

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 b_{4} -locally_euclidean TopSpace )

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 b

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

ex n being Nat st M is n -locally_euclidean

proof end;

registration

let n be Nat;

existence

ex b_{1} being non empty TopSpace st

( b_{1} is second-countable & b_{1} is Hausdorff & b_{1} is n -locally_euclidean )

end;
existence

ex b

( b

proof end;

definition
end;

notation
end;

registration

let n be Nat;

ex b_{1} being topological_manifold st

( b_{1} is n -dimensional & b_{1} is without_boundary )

end;
cluster non empty TopSpace-like T_0 T_1 T_2 second-countable V413() locally_euclidean n -dimensional without_boundary for TopStruct ;

existence ex b

( b

proof end;

registration

let n be non zero Nat;

ex b_{1} being topological_manifold st

( b_{1} is n -dimensional & b_{1} is compact & b_{1} is with_boundary )

end;
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 b

( b

proof end;

registration

let M be topological_manifold;

coherence

for b_{1} being non empty SubSpace of M holds

( b_{1} is second-countable & b_{1} is Hausdorff )

end;
coherence

for b

( b

proof end;

registration

let M1, M2 be topological_manifold;

coherence

( [:M1,M2:] is second-countable & [:M1,M2:] is T_2 ) ;

end;
coherence

( [:M1,M2:] is second-countable & [:M1,M2:] is T_2 ) ;