:: The Definition of Topological Manifolds :: by Marco Riccardi :: :: Received August 17, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin registration let x, y be set ; cluster{[x,y]} -> one-to-one ; correctness coherence {[x,y]} is one-to-one ; proofend; end; theorem Th1: :: MFOLD_1:1 for T being non empty TopSpace holds T,T | ([#] T) are_homeomorphic proofend; 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 number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) proofend; definition let n be Nat; let S be Subset of (TOP-REAL n); attrS is ball means :Def1: :: MFOLD_1:def 1 ex p being Point of (TOP-REAL n) ex r being real number 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 number 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 b1 being Subset of (TOP-REAL n) st b1 is ball ; proofend; cluster ball -> open for Element of bool the carrier of (TOP-REAL n); correctness coherence for b1 being Subset of (TOP-REAL n) st b1 is ball holds b1 is open ; proofend; end; registration let n be Nat; cluster non empty functional ball for Element of bool the carrier of (TOP-REAL n); correctness existence ex b1 being Subset of (TOP-REAL n) st ( not b1 is empty & b1 is ball ); proofend; 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 ) proofend; definition let n be Nat; let p be Point of (TOP-REAL n); let r be real number ; func Tball (p,r) -> SubSpace of TOP-REAL n equals :: MFOLD_1:def 2 (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_1:def_2_:_ for n being Nat for p being Point of (TOP-REAL n) for r being real number holds Tball (p,r) = (TOP-REAL n) | (Ball (p,r)); 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 ; ; let p be Point of (TOP-REAL n); let s be real positive number ; cluster Tball (p,s) -> non empty ; correctness coherence not Tball (p,s) is empty ; ; end; theorem Th4: :: MFOLD_1:4 for n being Nat for p being Point of (TOP-REAL n) for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r) proofend; 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 proofend; 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 proofend; :: like TOPREALB:19 theorem Th7: :: MFOLD_1:7 for n being Nat for p being Point of (TOP-REAL n) for r being real positive number 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 proofend; theorem Th8: :: MFOLD_1:8 for n being Nat holds Tunit_ball n, TOP-REAL n are_homeomorphic proofend; theorem Th9: :: MFOLD_1:9 for n being Nat for p, q being Point of (TOP-REAL n) for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic proofend; 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 proofend; 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 ) proofend; begin definition let n be Nat; let M be non empty TopSpace; attrM is n -locally_euclidean means :Def4: :: MFOLD_1:def 4 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 ; end; :: deftheorem Def4 defines -locally_euclidean MFOLD_1:def_4_:_ 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 ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ); registration let n be Nat; cluster TOP-REAL n -> n -locally_euclidean ; coherence TOP-REAL n is n -locally_euclidean proofend; end; registration let n be Nat; cluster non empty TopSpace-like n -locally_euclidean for TopStruct ; correctness existence ex b1 being non empty TopSpace st b1 is n -locally_euclidean ; proofend; end; Lm1: for n being Nat for M being non empty TopSpace st M is n -locally_euclidean 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 proofend; :: Lemma 2.13a theorem :: MFOLD_1:12 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 ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) proofend; :: Lemma 2.13b theorem Th13: :: MFOLD_1:13 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 U, [#] (TOP-REAL n) are_homeomorphic ) proofend; registration let n be Nat; cluster non empty TopSpace-like n -locally_euclidean -> non empty first-countable for TopStruct ; correctness coherence for b1 being non empty TopSpace st b1 is n -locally_euclidean holds b1 is first-countable ; proofend; 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 b1 being non empty TopSpace st b1 is 0 -locally_euclidean holds b1 is discrete proofend; cluster non empty TopSpace-like discrete -> non empty 0 -locally_euclidean for TopStruct ; coherence for b1 being non empty TopSpace st b1 is discrete holds b1 is 0 -locally_euclidean proofend; end; registration let n be Nat; cluster TOP-REAL n -> second-countable ; correctness coherence TOP-REAL n is second-countable ; proofend; 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 ) proofend; end; definition let n be Nat; let M be non empty TopSpace; attrM is n -manifold means :Def5: :: MFOLD_1:def 5 ( M is second-countable & M is Hausdorff & M is n -locally_euclidean ); end; :: deftheorem Def5 defines -manifold MFOLD_1:def_5_:_ 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 ) ); definition let M be non empty TopSpace; attrM is manifold-like means :Def6: :: MFOLD_1:def 6 ex n being Nat st M is n -manifold ; end; :: deftheorem Def6 defines manifold-like MFOLD_1:def_6_:_ for M being non empty TopSpace holds ( M is manifold-like iff ex n being Nat st M is n -manifold ); registration let n be Nat; cluster non empty TopSpace-like n -manifold for TopStruct ; existence ex b1 being non empty TopSpace st b1 is n -manifold proofend; 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 b1 being non empty TopSpace st b1 is n -manifold holds ( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean ); by Def5; cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean -> non empty n -manifold for TopStruct ; 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 ; by Def5; cluster non empty TopSpace-like n -manifold -> non empty manifold-like for TopStruct ; correctness coherence for b1 being non empty TopSpace st b1 is n -manifold holds b1 is manifold-like ; by Def6; end; registration cluster non empty TopSpace-like second-countable discrete -> non empty 0 -manifold for TopStruct ; coherence for b1 being non empty TopSpace st b1 is second-countable & b1 is discrete holds b1 is 0 -manifold ; end; :: Lemma 2.16 registration let n be Nat; let M be non empty n -manifold TopSpace; cluster non empty open -> non empty n -manifold for SubSpace of M; correctness coherence for b1 being non empty SubSpace of M st b1 is open holds b1 is n -manifold ; proofend; end; registration cluster non empty TopSpace-like manifold-like for TopStruct ; existence ex b1 being non empty TopSpace st b1 is manifold-like proofend; end; definition mode manifold is non empty manifold-like TopSpace; end;