:: by Marco Riccardi

::

:: Received August 17, 2010

:: Copyright (c) 2010-2012 Association of Mizar Users

begin

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 )

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 )

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

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;

correctness

existence

ex b_{1} being Subset of (TOP-REAL n) st b_{1} is ball ;

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} is ball holds

b_{1} is open ;

end;
correctness

existence

ex b

proof end;

correctness coherence

for b

b

proof end;

registration

let n be Nat;

correctness

existence

ex b_{1} being Subset of (TOP-REAL n) st

( not b_{1} is empty & b_{1} is ball );

end;
correctness

existence

ex b

( not b

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

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

let n be Nat;

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

let r be real number ;

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

correctness

coherence

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

;

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

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

:: deftheorem defines Tunit_ball MFOLD_1:def 3 :

for n being Nat holds Tunit_ball n = Tball ((0. (TOP-REAL n)),1);

for n being Nat holds Tunit_ball n = Tball ((0. (TOP-REAL n)),1);

registration

let n be Nat;

correctness

coherence

not Tunit_ball n is empty ;

;

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

let s be real positive number ;

correctness

coherence

not Tball (p,s) is empty ;

;

end;
correctness

coherence

not Tunit_ball n is empty ;

;

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

let s be real positive number ;

correctness

coherence

not Tball (p,s) is empty ;

;

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)

for p being Point of (TOP-REAL n)

for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r)

proof end;

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

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

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

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

proof end;

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

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

proof end;

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

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 )

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;

begin

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

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 ;

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

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;

correctness

existence

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

end;
correctness

existence

ex b

proof 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

proof end;

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

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 )

proof end;

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

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 )

proof end;

registration

let n be Nat;

correctness

coherence

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

b_{1} is first-countable ;

end;
correctness

coherence

for b

b

proof 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

coherence

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

b_{1} is discrete

for b_{1} being non empty TopSpace st b_{1} is discrete holds

b_{1} is 0 -locally_euclidean

end;
for b

b

proof end;

coherence for b

b

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

let n be Nat;

let M be non empty TopSpace;

end;
let M be non empty TopSpace;

attr M is n -manifold means :Def5: :: MFOLD_1:def 5

( M is second-countable & M is Hausdorff & M is n -locally_euclidean );

( M is second-countable & M is Hausdorff & M is n -locally_euclidean );

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

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

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

for M being non empty TopSpace holds

( M is manifold-like iff ex n being Nat st M is n -manifold );

registration
end;

registration

let n be Nat;

coherence

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

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

by Def5;

coherence

for b_{1} being non empty TopSpace st b_{1} is second-countable & b_{1} is Hausdorff & b_{1} is n -locally_euclidean holds

b_{1} is n -manifold ;

by Def5;

correctness

coherence

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

b_{1} is manifold-like ;

by Def6;

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

correctness coherence

for b

( b

by Def5;

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

correctness coherence

for b

b

by Def5;

correctness

coherence

for b

b

by Def6;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is second-countable & b_{1} is discrete holds

b_{1} is 0 -manifold
;

end;
for b

b

:: Lemma 2.16

registration

let n be Nat;

let M be non empty n -manifold TopSpace;

correctness

coherence

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

b_{1} is n -manifold ;

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

correctness

coherence

for b

b

proof end;