:: by Marco Riccardi

::

:: Received August 17, 2010

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

::$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,(TOP-REAL n) st

( ( for a being Point of X

for b being Point of (TOP-REAL n)

for r being Real 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 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 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 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

;

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

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

::$CT

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

for n being Nat

for p being Point of (TOP-REAL n)

for r being positive Real

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

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;

::$CT

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;

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 (TOP-REAL n) 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 (TOP-REAL n) 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 (TOP-REAL n) st U,S are_homeomorphic )

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 (TOP-REAL n) st U,S are_homeomorphic )

proof end;

registration

let n be Nat;

coherence

( TOP-REAL n is without_boundary & TOP-REAL n is n -locally_euclidean )

end;
coherence

( TOP-REAL n is without_boundary & TOP-REAL n is n -locally_euclidean )

proof 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 (TOP-REAL n) st U,B are_homeomorphic )

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 (TOP-REAL n) 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, [#] (TOP-REAL n) are_homeomorphic )

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, [#] (TOP-REAL n) are_homeomorphic )

proof end;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is without_boundary & b_{1} is locally_euclidean holds

b_{1} is first-countable ;

end;

cluster non empty TopSpace-like locally_euclidean without_boundary -> non empty first-countable for TopStruct ;

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;

definition

let n be Nat;

let M be non empty TopSpace;

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

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

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

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 b_{1} being non empty TopSpace st

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

end;
existence

ex b

( b

proof end;

registration

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

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

end;

cluster non empty TopSpace-like second-countable discrete -> non empty Hausdorff second-countable 0 -locally_euclidean for TopStruct ;

coherence for b

( b

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

;

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 ;

;

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

correctness coherence

for b

( b

;

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

correctness coherence

for b

b

;

:: Lemma 2.16

registration

let n be Nat;

let M be non empty without_boundary n -manifold TopSpace;

correctness

coherence

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

( b_{1} is without_boundary & b_{1} is n -manifold );

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

correctness

coherence

for b

( b

proof end;