:: The Definition of Topological Manifolds
:: by Marco Riccardi
::
:: Received August 17, 2010
:: Copyright (c) 2010-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3, SUPINF_2, XBOOLE_0, FUNCOP_1, ORDINAL2, TOPS_1, RCOMP_1, XXREAL_0, METRIC_1, TARSKI, STRUCT_0, REAL_1, COMPLEX1, SETFAM_1, PCOMPS_1, TOPS_2, T_0TOPSP, CONNSP_2, FUNCT_1, RELAT_1, CARD_1, SQUARE_1, TOPMETR, MEMBERED, XXREAL_1, XXREAL_2, WAYBEL23, COMPTS_1, RLVECT_3, NATTRA_1, ZFMISC_1, FRECHET, CARD_3, MFOLD_1, FUNCT_2, NAT_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, TOPS_2, RELAT_1, RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, STRUCT_0, PRE_TOPC, METRIC_1, TOPREAL9, TOPS_1, RLVECT_1, BORSUK_3, CONNSP_2, TSEP_1, METRIZTS, PCOMPS_1, COMPTS_1, EUCLID, SQUARE_1, TOPMETR, TMAP_1, XXREAL_1, MEMBERED, XXREAL_2, WAYBEL23, CANTOR_1, CARD_1, TDLAT_3, ZFMISC_1, CARD_3, YELLOW_8, FRECHET;
definitions TARSKI, FUNCT_1;
theorems TOPRNS_1, XREAL_0, TARSKI, FUNCT_2, EUCLID, XBOOLE_1, FUNCOP_1, JORDAN2C, XCMPLX_1, ABSVALUE, XXREAL_1, XXREAL_2, GOBOARD6, XREAL_1, RLVECT_1, ORDINAL1, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, CONNSP_2, METRIZTS, PCOMPS_1, T_0TOPSP, YELLOW14, TOPGRP_1, XBOOLE_0, TSEP_1, BORSUK_3, TOPREAL9, BORSUK_4, RELAT_1, FUNCT_1, TOPALG_1, TOPS_2, JGRAPH_1, RELSET_1, SQUARE_1, EUCLID_2, XXREAL_0, JGRAPH_2, TOPMETR, TOPREAL3, JORDAN6, GOBOARD9, RCOMP_1, JORDAN, WAYBEL23, YELLOW12, MEMBERED, JGRAPH_3, JGRAPH_5, TDLAT_3, FRECHET, CARD_3, YELLOW_8, RLVECT_4;
schemes FUNCT_2, TREES_2;
registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, MEMBERED, STRUCT_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TOPS_1, CARD_1, TSEP_1, TOPREAL9, COMPLEX1, TMAP_1, COMPTS_1, TOPMETR, XXREAL_2, METRIZTS, TOPREAL1, YELLOW13, KURATO_2, SUBSET_1, RELSET_1, FUNCT_2, SQUARE_1;
constructors HIDDEN, TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, TOPS_1, BORSUK_3, METRIZTS, COMPLEX1, BINOP_2, TMAP_1, WAYBEL23, CANTOR_1, TDLAT_3, YELLOW_8, FRECHET, SEQ_4, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XCMPLX_0, ALGSTR_0, STRUCT_0, PCOMPS_1, TOPREAL9, SQUARE_1, TMAP_1, WAYBEL23, ORDINAL1;
expansions TARSKI, FUNCT_1, WAYBEL23;


registration
let x, y be set ;
cluster {[x,y]} -> one-to-one ;
correctness
coherence
{[x,y]} is one-to-one ;
proof end;
end;

theorem Th1: :: MFOLD_1:1
for T being non empty TopSpace holds T,T | ([#] T) are_homeomorphic
proof end;

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

definition
let n be Nat;
let S be Subset of (TOP-REAL n);
attr S is ball means :Def1: :: MFOLD_1:def 1
 ex p being Point of (TOP-REAL n) 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 (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;
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 ;
proof end;
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 ;
;
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 );
proof end;
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 )
proof end;

definition
let n be Nat;
let p be Point of (TOP-REAL n);
let r be Real;
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 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 positive Real;
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 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
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
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 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;

theorem Th8: :: MFOLD_1:8
for n being Nat holds Tunit_ball n, TOP-REAL n are_homeomorphic
proof end;

theorem Th9: :: MFOLD_1:9
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
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
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;

definition
let n be Nat;
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 ;
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
proof end;
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 ;
proof end;
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 )
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 )
proof end;

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

registration
let n be Nat;
cluster TOP-REAL n -> second-countable ;
correctness
coherence
TOP-REAL n is second-countable ;
proof end;
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 )
proof end;
end;

definition
let n be Nat;
let M be non empty TopSpace;
attr M is n -manifold means :: MFOLD_1:def 5
( M is second-countable & M is Hausdorff & M is n -locally_euclidean );
end;

:: deftheorem 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;
attr M is manifold-like means :: MFOLD_1:def 6
 ex n being Nat st M is n -manifold ;
end;

:: deftheorem 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
proof end;
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 );
;
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 ;
;
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 ;
;
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 ;
proof end;
end;

registration
cluster non empty TopSpace-like manifold-like for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is manifold-like
proof end;
end;

definition
mode manifold is non empty manifold-like TopSpace;
end;