:: The Definition of Topological Manifolds
:: by Marco Riccardi
::
:: 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,() st ( ( for a being Point of X for b being Point of () 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 (); attr S is ball means :Def1: :: MFOLD_1:def 1 ex p being Point of () 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 () holds ( S is ball iff ex p being Point of () ex r being Real st S = Ball (p,r) ); registration let n be Nat; cluster functional ball for Element of bool the carrier of (); correctness existence ex b1 being Subset of () st b1 is ball ; proof end; cluster ball -> open for Element of bool the carrier of (); correctness coherence for b1 being Subset of () st b1 is ball holds b1 is open ; ; end; registration let n be Nat; cluster non empty functional ball for Element of bool the carrier of (); correctness existence ex b1 being Subset of () st ( not b1 is empty & b1 is ball ) ; proof end; end; theorem Th3: :: MFOLD_1:3 for n being Nat for p being Point of () for S being open Subset of () st p in S holds ex B being ball Subset of () 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. ()),1); correctness coherence Tball ((0. ()),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. ()),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 () st n <> 0 & p is Point of () holds
|.p.| < 1
proof end;

theorem Th6: :: MFOLD_1:6
for n being Nat
for f being Function of (),() st n <> 0 & ( for a being Point of ()
for b being Point of () st a = b holds
f . a = (1 / (1 - ())) * b ) holds
f is being_homeomorphism
proof end;

:: like TOPREALB:19
theorem :: MFOLD_1:7
for n being Nat
for p being Point of ()
for r being positive Real
for f being Function of (),(Tball (p,r)) st n <> 0 & ( for a being Point of ()
for b being Point of () 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 () holds B, [#] () 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 () 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 () 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 () st U,S are_homeomorphic )
proof end;

registration
let n be Nat;
coherence
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 () 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, [#] () are_homeomorphic )
proof end;

registration
correctness
coherence
for b1 being non empty TopSpace st b1 is without_boundary & b1 is locally_euclidean holds
b1 is first-countable
;
proof end;
end;

set T = () | ([#] ());

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

registration
coherence
for b1 being non empty TopSpace st b1 is 0 -locally_euclidean holds
b1 is discrete
proof end;
coherence
for b1 being non empty TopSpace st b1 is discrete holds
b1 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;
existence
ex b1 being non empty TopSpace st
( b1 is without_boundary & b1 is n -manifold )
proof end;
end;

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

registration
let n be Nat;
correctness
coherence
for b1 being non empty TopSpace st b1 is n -manifold holds
( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean )
;
;
correctness
coherence
for b1 being non empty TopSpace st b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean holds
b1 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 b1 being non empty SubSpace of M st b1 is open holds
( b1 is without_boundary & b1 is n -manifold )
;
proof end;
end;