:: Topological Manifolds
:: by Karol P\k{a}k
::
:: Received June 16, 2014
:: Copyright (c) 2014 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_1, ARYTM_3, BROUWER, CARD_1, COMPLEX1, EUCLID, FUNCT_1,
METRIC_1, NAT_1, NUMBERS, ORDINAL1, PCOMPS_1, PRE_TOPC, RCOMP_1, RELAT_1,
STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPS_1, TOPS_2, XBOOLE_0, XREAL_0,
XXREAL_0, XCMPLX_0, FINSET_1, ZFMISC_1, REAL_1, SETFAM_1, T_0TOPSP,
CONNSP_2, MFOLD_1, RELAT_2, EQREL_1, CONNSP_1, CONNSP_3, MFOLD_0,
WAYBEL23, COMPTS_1, RLVECT_3;
notations TARSKI, XBOOLE_0, FINSET_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
XXREAL_3, NAT_1, CARD_1, REAL_1, SETFAM_1, STRUCT_0, PRE_TOPC, TOPS_1,
METRIC_1, PCOMPS_1, RLVECT_1, EUCLID, TOPREAL9, TOPS_2, CONNSP_1,
CONNSP_2, CONNSP_3, COMPTS_1, BROUWER, DOMAIN_1, ZFMISC_1, MFOLD_1,
BORSUK_1, BORSUK_2, NAT_D, BINOP_1, EQREL_1, BORSUK_3, WAYBEL23,
CANTOR_1;
constructors MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1, FUNCSDOM, BROUWER,
SEQ_4, EUCLID_9, SIMPLEX0, CONNSP_1, CONNSP_3, BORSUK_3, MFOLD_1, NAT_D,
BORSUK_2, WAYBEL23, CANTOR_1, REAL_1;
registrations BORSUK_1, BROUWER, EUCLID, FUNCT_1, FUNCT_2, NAT_1, PRE_TOPC,
RELAT_1, SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPS_1, XBOOLE_0,
XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TOPREALC, CARD_1, TOPREAL9,
XXREAL_3, MFOLD_1, BORSUK_3, WAYBEL_2, XCMPLX_0, JORDAN1, BORSUK_2,
CONNSP_1, ORDINAL1, METRIZTS, COMPTS_1, TOPREAL1;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
definitions TARSKI, XBOOLE_0;
equalities BINOP_1, STRUCT_0, XCMPLX_0, TOPREAL9, BROUWER, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorems ABSVALUE, BORSUK_1, BROUWER, COMPTS_1, CONNSP_2, EUCLID, FUNCT_1,
FUNCT_2, GOBOARD6, JORDAN24, JORDAN2C, ORDINAL1, PRE_TOPC, RELAT_1,
RLVECT_1, SUBSET_1, TARSKI, TOPMETR, TOPREAL9, TOPRNS_1, TOPS_1, TOPS_2,
XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1, CARD_1, TSEP_1,
SETFAM_1, BROUWER2, NAT_1, TOPGRP_1, JORDAN, METRIZTS, T_0TOPSP, MFOLD_1,
BORSUK_3, EUCLID_2, TOPREALA, FUNCT_3, EQREL_1, TIETZE_2, CONNSP_1,
CONNSP_3, CARD_2, WAYBEL23, YELLOW12, BROUWER3;
schemes FUNCT_2, NAT_1, CLASSES1;
begin :: Preliminaries
reserve n,m for Nat;
Lm1:for p,q be Point of TOP-REAL n
for r,s be real number st
r>0 & s>0 holds Tdisk(p,r),Tdisk(q,s) are_homeomorphic
proof
set TR=TOP-REAL n;
let p,q be Point of TR;
let r,s be real number;
assume that
A1: r>0
and
A2: s>0;
Ball(q,s) c= Int cl_Ball(q,s) by TOPREAL9: 16,TOPS_1:24;
then A3: cl_Ball(q,s) is non boundary compact by A2;
Ball(p,r) c= Int cl_Ball(p,r) by TOPREAL9: 16,TOPS_1:24;
then cl_Ball(p,r) is non boundary compact by A1;
then ex h be Function of TR |cl_Ball(p,r),TR |cl_Ball(q,s) st
h is being_homeomorphism & h.:Fr cl_Ball(p,r) = Fr cl_Ball(q,s)
by A3,BROUWER2:7;
hence thesis by T_0TOPSP:def 1;
end;
theorem
for M be non empty TopSpace
for q be Point of M,r be real number,p be Point of TOP-REAL n st r>0
for U be a_neighborhood of q st M|U,Tball(p,r) are_homeomorphic
ex W being a_neighborhood of q st
W c= Int U & M|W,Tdisk(p,r) are_homeomorphic
proof
let M be non empty TopSpace;
set TR=TOP-REAL n;
let q be Point of M,r be real number,p be Point of TR such that
A1: r>0;
let U be a_neighborhood of q such that
A2: M|U,Tball(p,r) are_homeomorphic;
A3: [#](M|U)=U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
set MU=M|U;
consider h be Function of MU,Tball(p,r) such that
A4: h is being_homeomorphism by T_0TOPSP:def 1,A2;
A5:dom h =[#](M|U) by A4,TOPS_2:def 5;
A6:Tball(p,r)=TR|Ball(p,r) by MFOLD_1:def 2;
then
A7: [#]Tball(p,r) = Ball(p,r) by PRE_TOPC:def 5;
then reconsider W=h.:IU as Subset of TR by XBOOLE_1:1;
IU is open by TSEP_1:9;
then h .: IU is open by A4,TOPGRP_1:25,A1;
then reconsider W as open Subset of TR by A7,TSEP_1:9;
q in Int U by CONNSP_2:def 1;
then
A8: h.q in W by A5,FUNCT_1:def 6;
then reconsider hq=h.q as Point of TR;
reconsider HQ=hq as Point of Euclid n by EUCLID:67;
Int W=W by TOPS_1:23;
then consider s be Real such that
A9: s>0
and
A10: Ball(HQ,s) c= W by A8,GOBOARD6:5;
set m=s/2;
A11: Ball(HQ,s)=Ball(hq,s) by TOPREAL9:13;
set CL=cl_Ball(hq,m);
N: n in NAT by ORDINAL1:def 12;
A12: CL c= Ball(hq,s) by A9,N,XREAL_1:216,JORDAN:21;
then CL c= W by A10,A11;
then
A14: CL c= Ball(p,r) by A7,XBOOLE_1:1;
set BB = Ball(hq,m);
A15: BB c= CL by TOPREAL9:16;
then reconsider CL,BB as Subset of Tball(p,r) by A14,XBOOLE_1:1,A7;
A16: rng h = [#]Tball(p,r) by A4,TOPS_2:def 5;
A17: q in Int U by CONNSP_2:def 1;
A18: Int U c= U by TOPS_1:16;
reconsider hBB=h"BB as Subset of M by A3,XBOOLE_1:1;
hq is Element of REAL n by EUCLID:22;
then |. hq-hq .|=0;
then hq in BB by A9;
then
A19:q in hBB by FUNCT_1:def 7,A5,A18,A17,A3;
SS:dom h = [#]MU by A4,TOPS_2:def 5;
A21:h"W = IU by FUNCT_1:82,A4,FUNCT_1:76,SS;
CL meets Ball(p,r) by A9,A7,XBOOLE_1:67;
then reconsider hCL=h"CL as non empty Subset of MU by A7,RELAT_1:138,A16;
A22: h.:hCL = CL by FUNCT_1:77,A16;
A23: Tball(p,r) | CL = TR|cl_Ball(hq,m) by A6,A7,PRE_TOPC:7;
then reconsider HH=h|hCL as Function of MU|hCL,Tdisk(hq,m)
by A22,A1,JORDAN24:12;
HH is being_homeomorphism by A22,A23,A4,METRIZTS:2;
then
A24: MU|hCL,Tdisk(hq,m) are_homeomorphic by T_0TOPSP:def 1;
Tdisk(hq,m),Tdisk(p,r) are_homeomorphic by A1,A9,Lm1;
then
A25: MU|hCL,Tdisk(p,r) are_homeomorphic by A1,A9,BORSUK_3:3,A24;
reconsider HCL=hCL as Subset of M by A3,XBOOLE_1:1;
A26: MU|hCL=M|HCL by PRE_TOPC:7,A3;
BB c= W by A10,A11,A12,A15;
then
A27: h"BB c= h"W by RELAT_1:143;
BB is open by TSEP_1:9;
then h"BB is open by A4,TOPGRP_1:26,A1;
then hBB is open by A21,A27,TSEP_1:9;
then q in Int HCL by RELAT_1:143,A15,A19,TOPS_1:22;
then
A28: HCL is a_neighborhood of q by CONNSP_2:def 1;
CL c= W by A12,A10,A11;
hence thesis by A28,RELAT_1:143,A21,A25,A26;
end;
begin :: Locally Euclidean Spaces
reserve M,M1,M2 for non empty TopSpace;
definition
let M;
attr M is locally_euclidean means :Def1:
for p being Point of M
ex U being a_neighborhood of p, n st
M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic;
end;
definition
let n,M;
attr M is n-locally_euclidean means :Def2:
for p being Point of M
ex U being a_neighborhood of p st
M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic;
end;
registration
let n;
cluster Tdisk(0.TOP-REAL n,1) -> n-locally_euclidean;
coherence
proof
let p be Point of Tdisk(0.TOP-REAL n,1);
Int [#]Tdisk(0.TOP-REAL n,1) = [#]Tdisk(0.TOP-REAL n,1) by TOPS_1:15;
then reconsider CM=[#]Tdisk(0.TOP-REAL n,1) as
non empty a_neighborhood of p by CONNSP_2:def 1;
take CM;
thus thesis by TSEP_1:93;
end;
end;
registration
let n;
cluster n-locally_euclidean for non empty TopSpace;
existence
proof
take M=Tdisk(0.TOP-REAL n,1);
thus thesis;
end;
end;
registration
let n;
cluster n-locally_euclidean -> locally_euclidean
for non empty TopSpace;
coherence
proof
let M be non empty TopSpace;
assume A1:M is n-locally_euclidean;
let p be Point of M;
ex U be a_neighborhood of p st M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic
by A1;
hence thesis;
end;
end;
begin :: Locally Euclidean Spaces With and Without a Boundary
definition
let M be locally_euclidean non empty TopSpace;
func Int M -> Subset of M means :Def3:
for p be Point of M holds
p in it
iff
ex U being a_neighborhood of p, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
existence
proof
set I = {p where p is Point of M:ex U being a_neighborhood of p, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic};
I c= the carrier of M
proof
let x be object;
assume x in I;
then ex q be Point of M st x=q & ex U being a_neighborhood of q, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
hence thesis;
end;
then reconsider I as Subset of M;
take I;
let p be Point of M;
hereby
assume p in I;
then ex q be Point of M st p=q & ex U being a_neighborhood of q, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
hence ex U being a_neighborhood of p, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
end;
thus thesis;
end;
uniqueness
proof
let I1,I2 be Subset of M such that
A1: for p be Point of M holds p in I1 iff
ex U being a_neighborhood of p, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
and
A2: for p be Point of M holds p in I2 iff
ex U being a_neighborhood of p, n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
hereby
let x be object;
assume
A3: x in I1;
then reconsider p=x as Point of M;
ex U being a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A3,A1;
hence x in I2 by A2;
end;
let x be object;
assume
A4: x in I2;
then reconsider p=x as Point of M;
ex U being a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A4,A2;
hence x in I1 by A1;
end;
end;
registration
let M be locally_euclidean non empty TopSpace;
cluster Int M -> non empty open;
coherence
proof
A1: for x be set holds x in Int M iff
ex U be Subset of M st U is open & U c=Int M & x in U
proof
let x be set;
hereby
assume
A2: x in Int M;
then reconsider p=x as Point of M;
consider U be a_neighborhood of p,n such that
A3: M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A2,Def3;
take W=Int U;
W c= Int M
proof
let y be object;
assume
A4: y in W;
then reconsider q=y as Point of M;
U is a_neighborhood of q by A4,CONNSP_2:def 1;
hence thesis by Def3,A3;
end;
hence W is open & W c= Int M & x in W by CONNSP_2:def 1;
end;
thus thesis;
end;
set p = the Point of M;
consider U be a_neighborhood of p, n such that
A7: M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def1;
A8: [#](M|U)=U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
set MU=M|U;
set TR=TOP-REAL n;
consider h be Function of MU,Tdisk(0.TR,1) such that
A9: h is being_homeomorphism by T_0TOPSP:def 1,A7;
IU is open by TSEP_1:9;
then h.:IU is open by A9,TOPGRP_1:25;
then h.:IU in the topology of Tdisk(0.TR,1) by PRE_TOPC:def 2;
then consider W be Subset of TR such that
A10: W in the topology of TR
and
A11: h.:IU = W/\[#]Tdisk(0.TR,1) by PRE_TOPC: def 4;
A12: [#]Tdisk(0.TR,1) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
A13: dom h = [#]MU by A9,TOPS_2:def 5;
A15: Ball(0.TR,1) c= cl_Ball(0.TR,1) by TOPREAL9:16;
reconsider W as open Subset of TR by A10,PRE_TOPC:def 2;
set WB=W/\Ball(0.TR,1);
p in Int U by CONNSP_2:def 1;
then
A16: h.p in h.:IU by A13,FUNCT_1:def 6;
then
A17: h.p in W by A11,XBOOLE_0:def 4;
then reconsider hp=h.p as Point of TR;
A18: h .: IU = W/\cl_Ball(0.TR,1) by PRE_TOPC:def 5,A11;
WB is non empty
proof
reconsider HP=hp as Point of Euclid n by EUCLID:67;
A19: Ball(0.TR,1) misses Sphere(0.TR,1) by TOPREAL9:19;
A20: cl_Ball(0.TR,1) = Ball(0.TR,1)\/Sphere(0.TR,1) by TOPREAL9:18;
assume
A21: WB is empty;
then (W/\cl_Ball(0.TR,1))= (W/\cl_Ball(0.TR,1))\WB
.=((W/\cl_Ball(0.TR,1))\W) \/((W/\cl_Ball(0.TR,1))\Ball(0.TR,1))
by XBOOLE_1: 54
.= {}\/((W/\cl_Ball(0.TR,1))\Ball(0.TR,1)) by XBOOLE_1:17,37
.= W/\ (cl_Ball(0.TR,1)\Ball(0.TR,1)) by XBOOLE_1:49
.= W/\ Sphere(0.TR,1) by A19,A20,XBOOLE_1:88;
then hp in Sphere(0.TR,1) by A18,A16,XBOOLE_0:def 4;
then
A22: |.hp.| = 1 by TOPREAL9:12;
Int W=W by TOPS_1:23;
then consider s be Real such that
A23: s>0
and
A24: Ball(HP,s) c= W by A17,GOBOARD6:5;
set s2=s/2,m=min(s/2,1/2);
A25: m <=s2 by XXREAL_0:17;
s2 ~~0 by A23,XXREAL_0:21;
then
A29: 1-m < 1-0 by XREAL_1:6;
A30: |. -m .|=--m by A28,ABSVALUE:def 1;
A31: (1-m)*hp-0.TR = (1-m)*hp by RLVECT_1:13;
(1-m)*hp - hp = (1-m)*hp - 1*hp by RLVECT_1:def 8
.= ((1-m)-1)*hp by RLVECT_1:35
.= (-m) *hp;
then |.(1-m)*hp - hp.| = |. -m .|*1 by A22,EUCLID:11;
then
A32: ( 1-m)*hp in Ball(hp,s) by A30,A26;
1-m >= 1-1/2 by XXREAL_0:17,XREAL_1:10;
then |.1-m .|=1-m by ABSVALUE:def 1;
then |. (1-m)*hp.| = (1-m)*1 by A22,EUCLID:11;
then (1-m)*hp in Ball(0.TR,1) by A31,A29;
hence thesis by A32,A24,A27,A21,XBOOLE_0:def 4;
end;
then consider wb be set such that
A33: wb in WB;
reconsider wb as Point of TR by A33;
reconsider wbE=wb as Point of Euclid n by EUCLID:67;
Int WB=WB by TOPS_1:23;
then consider s be Real such that
A34: s>0
and
A35: Ball(wbE,s) c= WB by A33,GOBOARD6:5;
A36:Ball(wb,s)=Ball(wbE,s) by TOPREAL9:13;
WB c= Ball(0.TR,1) by XBOOLE_1:17;
then
A37: Ball(wb,s) c= Ball(0.TR,1) by A35,A36;
then
reconsider BB=Ball(wb,s) as Subset of Tdisk(0.TR,1) by A15,XBOOLE_1:1,A12;
A38: Tdisk(0.TR,1) | BB = TR|Ball(wb,s) by A37,A15,XBOOLE_1:1,PRE_TOPC:7;
reconsider hBB=h"BB as Subset of M by A8,XBOOLE_1:1;
BB is open by TSEP_1:9;
then
A39:h"BB is open by A9,TOPGRP_1:26;
WB c= h .: IU by A12,A11,TOPREAL9:16,XBOOLE_1:26;
then BB c= h.:IU by A35,A36;
then
A40: h"BB c= h"(h.:IU) by RELAT_1:143;
h"(h.:IU)c= IU by FUNCT_1:82,A9;
then h"BB c= IU by A40;
then hBB is open by A39,TSEP_1:9;
then
A41: Int hBB = hBB by TOPS_1:23;
A42: rng h = [#]Tdisk(0.TR,1) by A9,TOPS_2:def 5;
then
A43: h.:(h"BB)=BB by FUNCT_1:77;
hBB is non empty by A34,RELAT_1:139,A42;
then consider t be set such that
A44: t in hBB;
reconsider t as Point of M by A44;
reconsider hBB as a_neighborhood of t by A41,CONNSP_2:def 1,A44;
A45: TR|Ball(wb,s) = Tball(wb,s) by MFOLD_1:def 2;
A46: MU|h"BB =M|hBB by A8,PRE_TOPC:7;
then reconsider HH=h|h"BB as Function of M|hBB,TR|Ball(wb,s)
by A43,A38,JORDAN24:12;
HH is being_homeomorphism by A9,A43,A38,A46,METRIZTS:2;
then
A47:M|hBB,TR|Ball(wb,s) are_homeomorphic by T_0TOPSP:def 1;
Tball(wb,s), Tball(0.TR,1) are_homeomorphic by MFOLD_1:9,A34;
then M|hBB,Tball(0.TR,1) are_homeomorphic by A47,A45,A34,BORSUK_3:3;
hence thesis by A1,TOPS_1:25,Def3;
end;
end;
definition
let M be locally_euclidean non empty TopSpace;
func Fr M -> Subset of M equals (Int M)`;
coherence;
end;
::$N Boundary Points of Locally Euclidean Spaces
theorem Th3:
for M be locally_euclidean non empty TopSpace
for p be Point of M holds
p in Fr M
iff
ex U being a_neighborhood of p,
n be Nat,
h be Function of M|U,Tdisk(0.TOP-REAL n,1)
st h is being_homeomorphism & h.p in Sphere(0.TOP-REAL n,1)
proof
let M be locally_euclidean non empty TopSpace;
let p be Point of M;
thus p in Fr M implies ex U be a_neighborhood of p,n be Nat,
h be Function of M| U,Tdisk(0.TOP-REAL n,1) st
h is being_homeomorphism & h.p in Sphere(0.TOP-REAL n,1)
proof
assume
A1: p in Fr M;
consider U be a_neighborhood of p, n such that
A2: M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def1;
set TR=TOP-REAL n;
consider h be Function of M|U,Tdisk(0.TR,1) such that
A3: h is being_homeomorphism by A2,T_0TOPSP:def 1;
assume for U be a_neighborhood of p,n be Nat, h be Function of M|U,
Tdisk(0.TOP-REAL n,1) st h is being_homeomorphism holds
not h.p in Sphere(0.TOP-REAL n,1);
then
A4: not h.p in Sphere(0.TR,1) by A3;
A5: Ball(0.TR,1) in the topology of TR by PRE_TOPC:def 2;
A6: p in Int U by CONNSP_2:def 1;
A7: Int U in the topology of M by PRE_TOPC:def 2;
A8: [#](M|U) = U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
IU/\U = IU by TOPS_1:16,XBOOLE_1:28;
then IU in the topology of M|U by A7,A8,PRE_TOPC:def 4;
then reconsider IU as non empty open Subset of M|U
by CONNSP_2:def 1,PRE_TOPC:def 2;
A9: [#](TR|cl_Ball(0.TR,1)) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider hIU=h.:IU as Subset of TR by XBOOLE_1:1;
A10: h.:IU is open by A3,TOPGRP_1:25;
A11: dom h = [#](M|U) by A3,TOPS_2:def 5;
then
A12: h"(h.:IU) = IU by FUNCT_1:94,A3;
A13: cl_Ball(0.TR,1) = Ball(0.TR,1) \/ Sphere(0.TR,1) by TOPREAL9:18;
then reconsider B=Ball(0.TR,1) as Subset of TR|cl_Ball(0.TR,1)
by A9,XBOOLE_1:7;
Ball(0.TR,1) /\ cl_Ball(0.TR,1) = Ball(0.TR,1) by A13,XBOOLE_1:7,28;
then B in the topology of TR|cl_Ball(0.TR,1) by A5,A9,PRE_TOPC:def 4;
then reconsider B as non empty open Subset of TR|cl_Ball(0.TR,1)
by PRE_TOPC:def 2;
reconsider BhIU = B /\ (h.:IU) as Subset of TR by XBOOLE_1:1,A9;
BhIU c= Ball(0.TR,1) by XBOOLE_1:17;
then
A14: BhIU is open by A10,TSEP_1:9;
A15: Int U c= U by TOPS_1:16;
then h.p in rng h by A6,A8,A11,FUNCT_1:def 3;
then
A16:h.p in Ball(0.TR,1) by A4,A9,A13,XBOOLE_0:def 3;
then reconsider hp=h.p as Point of TR;
the TopStruct of TR=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider HP=hp as Point of Euclid n by TOPMETR:12;
h.p in h.:IU by A11,A6,FUNCT_1:def 6;
then h.p in BhIU by A16,XBOOLE_0:def 4;
then hp in Int(BhIU) by A14,TOPS_1:23;
then consider s be Real such that
A17: s>0
and
A18: Ball(HP,s) c= BhIU by GOBOARD6:5;
set W=Ball(hp,s);
reconsider hW=h"W as Subset of M by A8,XBOOLE_1:1;
A19:W c= B /\ (h.:IU) by A18,TOPREAL9:13;
then reconsider w=W as Subset of TR|cl_Ball(0.TR,1) by XBOOLE_1:1;
A20:w in the topology of TR by PRE_TOPC:def 2;
hp is Element of REAL n by EUCLID:22;
then |. hp-hp .|=0;
then hp in Ball(hp,s) by A17;
then
A21: p in hW by A8,A11,A15,A6,FUNCT_1:def 7;
rng h = [#](TR|cl_Ball(0.TR,1)) by A3,TOPS_2:def 5;
then h.:(h"W) = W by A19,XBOOLE_1:1,FUNCT_1:77;
then
A22: Tdisk(0.TR,1) | (h.:(h"W)) = TR|W by A9,PRE_TOPC:7;
w/\cl_Ball(0.TR,1) = w by A9,XBOOLE_1:28;
then
A23: w in the topology of TR |cl_Ball(0.TR,1) by A9,A20,PRE_TOPC:def 4;
B /\ (h.:IU) c= h.:IU by XBOOLE_1:17;
then W c= h.:IU by A19;
then
A24: hW c= IU by A12,RELAT_1:143;
reconsider w as open Subset of TR |cl_Ball(0.TR,1) by A23,PRE_TOPC:def 2;
reconsider hh=h| (h"w) as Function of (M|U) |h"w,
Tdisk(0.TR,1) | (h.:(h"w)) by JORDAN24:12;
A25: (M|U) |h"W = M|hW by A8,PRE_TOPC:7;
then reconsider HH=hh as Function of M|hW, TR|W by A22;
h"w is open by A3,TOPGRP_1:26;
then hW is open by A24,TSEP_1:9;
then p in Int hW by A21,TOPS_1:23;
then reconsider HW=hW as a_neighborhood of p by CONNSP_2:def 1;
A26:TR|W = Tball(hp,s) by MFOLD_1:def 2;
HH is being_homeomorphism by A3,METRIZTS:2,A22,A25;
then
A27: M|HW, TR|W are_homeomorphic by T_0TOPSP:def 1;
Tball(hp,s),Tball(0.TR,1) are_homeomorphic by A17,MFOLD_1:9;
then M|HW, Tball(0.TR,1) are_homeomorphic by A27,A26,A17,BORSUK_3:3;
then p in Int M by Def3;
then not p in [#]M\ Int M by XBOOLE_0:def 5;
hence contradiction by SUBSET_1:def 4,A1;
end;
given U be a_neighborhood of p, n be Nat, h be Function of M|U,
Tdisk(0.TOP-REAL n,1) such that
A28: h is being_homeomorphism
and
A29: h.p in Sphere(0.TOP-REAL n,1);
set TR=TOP-REAL n;
A30: p in Int U by CONNSP_2:def 1;
assume not p in Fr M;
then not p in [#]M\Int M by SUBSET_1:def 4;
then p in Int M by XBOOLE_0:def 5;
then consider W be a_neighborhood of p,m such that
A31: M|W,Tball(0.TOP-REAL m,1) are_homeomorphic by Def3;
A:Tball(0.TOP-REAL m,1) = (TOP-REAL m) |Ball(0.TOP-REAL m,1) by MFOLD_1:def 2;
A32: p in Int W by CONNSP_2:def 1;
M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A28,T_0TOPSP:def 1;
then m=n by A30,A32,XBOOLE_0:3,A,BROUWER3:15,A31;
then M|W,TR|Ball(0.TR,1) are_homeomorphic by A31,MFOLD_1:def 2;
then consider g be Function of M|W,TR|Ball(0.TR,1) such that
A33: g is being_homeomorphism by T_0TOPSP:def 1;
A34: Int U c= U by TOPS_1:16;
set I = (Int U)/\Int W;
A35: [#](M|U)=U by PRE_TOPC:def 5;
I c= Int U by XBOOLE_1:17;
then reconsider IU = I as non empty open Subset of (M|U)
by XBOOLE_1:1,A34,A35,A30,A32,XBOOLE_0:def 4,TSEP_1:9;
A36: dom h = [#](M|U) by A28,TOPS_2:def 5;
then
A37: h"(h.:IU) = IU by A28,FUNCT_1:94;
p in I by A30,A32,XBOOLE_0:def 4;
then
A38: h.p in h.:IU by A36,FUNCT_1:def 6;
h.:IU is open by A28,TOPGRP_1:25;
then h.:IU in the topology of TR|cl_Ball(0.TR,1) by PRE_TOPC:def 2;
then consider Q be Subset of TR such that
A39: Q in the topology of TR
and
A40: h.:IU = Q /\[#](TR|cl_Ball(0.TR,1)) by PRE_TOPC: def 4;
reconsider Q as non empty Subset of TR by A40;
A41: Int Q=Q by A39,PRE_TOPC:def 2,TOPS_1:23;
A42: I c= Int W by XBOOLE_1:17;
A43: [#] (TR|cl_Ball(0.TR,1)) = cl_Ball(0.TR,1) by PRE_TOPC :def 5;
then h.p in cl_Ball(0.TR,1) by A38;
then reconsider hp=h.p as Point of TR;
the TopStruct of TR=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider HP=hp as Point of Euclid n by TOPMETR:12;
hp in Q by A38,A40,XBOOLE_0:def 4;
then consider s be Real such that
A44: s>0
and
A45: Ball(HP,s) c= Q by A41,GOBOARD6:5;
set s2=s/2;
hp is Element of REAL n by EUCLID:22;
then |. hp-hp .|=0;
then
A46:hp in Ball(hp,s2) by A44;
set clb = cl_Ball(hp,s2)/\cl_Ball(0.TR,1);
A47: Ball(hp,s2) c= cl_Ball(hp,s2) by TOPREAL9:16;
clb = cl_Ball(hp,s2)/\[#](TR|cl_Ball(0.TR,1)) by PRE_TOPC :def 5;
then reconsider CLB = clb as non empty Subset of TR|cl_Ball(0.TR,1)
by A47,A46,A38,XBOOLE_0:def 4;
A48: rng h = [#] (TR|cl_Ball(0.TR,1)) by A28,TOPS_2:def 5;
then reconsider hCLB=h"CLB as non empty Subset of M|U by RELAT_1:139;
A49:Ball(HP,s)=Ball(hp,s) by TOPREAL9:13;
hp in CLB by A47,A46,A38,A43,XBOOLE_0:def 4;
then
A50: p in hCLB by A36,A35,A34,A30,FUNCT_1:def 7;
n in NAT by ORDINAL1:def 12;
then
A51: cl_Ball(hp,s2) c= Ball(hp,s) by XREAL_1:216,A44,JORDAN:21;
then cl_Ball(hp,s2) c= Q by A45,A49;
then CLB c= h.:IU by A43,XBOOLE_1:26,A40;
then
A52: hCLB c= IU by RELAT_1:143,A37;
reconsider BB = Ball(hp,s2)/\[#](TR|cl_Ball(0.TR,1)) as
Subset of TR|cl_Ball(0.TR,1);
reconsider hBB =h"BB as Subset of M by A35,XBOOLE_1:1;
Ball(hp,s2) c= Q by A45,A49,A47,A51;
then BB c= h.:IU by XBOOLE_1:26,A40;
then
A53: h"BB c= IU by RELAT_1: 143,A37;
reconsider HCLB=hCLB as non empty Subset of M by A35,XBOOLE_1:1;
A54: h.:hCLB = CLB by A48,FUNCT_1:77;
A55:(TR|cl_Ball(0.TR,1)) |CLB = TR|clb by A43,PRE_TOPC:7;
A56:(M|U) |hCLB = M|HCLB by A35,PRE_TOPC:7;
then reconsider h1=h|hCLB as Function of M|HCLB,TR|clb
by A55,A54,JORDAN24:12;
A57: Int W c= W by TOPS_1:16;
A58: [#](M|W)=W by PRE_TOPC:def 5;
then reconsider IW = I as non empty open Subset of (M|W)
by A30,A32,XBOOLE_0:def 4,XBOOLE_1:1,A57,A42,TSEP_1:9;
A59: IU c= W by A57,A42;
then reconsider hCLW=hCLB as non empty Subset of M|W by A52,XBOOLE_1:1,A58;
A60:(M|W) |hCLW = M|HCLB by A52,A59,XBOOLE_1:1,PRE_TOPC:7;
set ghCLW = g.:hCLW;
A61: [#] (TR|Ball(0.TR,1)) = Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider GhCLW = ghCLW as non empty Subset of TR by XBOOLE_1:1;
A62:(TR|Ball(0.TR,1)) | ghCLW = TR|GhCLW by A61,PRE_TOPC:7;
then reconsider g1=g|hCLB as Function of M|HCLB,TR|GhCLW by A60,JORDAN24:12;
A63:g1 is being_homeomorphism by A33,METRIZTS:2,A62,A60;
then
A64:g1" is being_homeomorphism by TOPS_2:56;
A65: dom g = [#](M|W) by A33,TOPS_2:def 5;
then g.p in GhCLW by A50,FUNCT_1:def 6;
then reconsider gp=g.p as Point of TR;
I c= W by A57,A42;
then reconsider hBW=hBB as Subset of (M|W) by A53,XBOOLE_1:1,A58;
reconsider ghBW=g.:hBW as Subset of TR by A61,XBOOLE_1:1;
hp in BB by A46,A38,XBOOLE_0:def 4;
then p in h"BB by A36,A35,A34,A30,FUNCT_1:def 7;
then
A66:gp in ghBW by A65,FUNCT_1:def 6;
set hg= h1*(g1");
h1 is being_homeomorphism by A28,A55,METRIZTS:2,A56,A54;
then
A67:hg is being_homeomorphism by A64,TOPS_2:57;
then
A68: dom hg = [#](TR|GhCLW) by TOPS_2:def 5;
BB c= clb by TOPREAL9:16,XBOOLE_1:26,A43;
then
A69: hBB c= hCLB by RELAT_1:143;
then ghBW c= GhCLW by RELAT_1:123;
then gp in GhCLW by A66;
then
A70:gp in dom hg by A68,PRE_TOPC:def 5;
Ball(hp,s2) in the topology of TR by PRE_TOPC:def 2;
then BB in the topology of TR|cl_Ball(0.TR,1) by PRE_TOPC:def 4;
then BB is non empty open by A46,A38,XBOOLE_0:def 4,PRE_TOPC:def 2;
then h"BB is open by A28,TOPGRP_1:26;
then hBB is open by A53,TSEP_1:9;
then hBW is open by TSEP_1:9;
then g.:hBW is open by A33,TOPGRP_1:25;
then ghBW is open by A61,TSEP_1:9;
then gp in Int GhCLW by A66,TOPS_1:22,A69,RELAT_1:123;
then
A71: hg.gp in Int clb by BROUWER3:11,A67;
Int clb = (Int cl_Ball(hp,s2)) /\ Int cl_Ball(0.TR,1) by TOPS_1:17;
then
A72: hg.gp in Int cl_Ball(0.TR,1) by A71,XBOOLE_0:def 4;
reconsider G1=g1 as Function;
Fr cl_Ball(0.TR,1) = Sphere(0.TR,1) by BROUWER2:5;
then
A73:Int cl_Ball(0.TR,1) = cl_Ball(0.TR,1)\Sphere(0.TR,1) by TOPS_1:40;
A74:G1"=g1" by A63,TOPS_2:def 4;
dom g1 = [#](M|HCLB) by A63,TOPS_2:def 5;
then p in dom g1 by PRE_TOPC:def 5,A50;
then
A75: (g1".(g1.p)) = p by A63,A74,FUNCT_1:34;
A76:g.p = g1.p by A50, FUNCT_1:49;
then
A77: p in dom h1 by A70,FUNCT_1:11,A75;
hg.gp = h1.p by A70,FUNCT_1:12,A75,A76;
then hg.gp = h.p by A77,FUNCT_1:47;
hence contradiction by A29, A72,A73,XBOOLE_0:def 5;
end;
begin :: Interior and Boundary of Locally Euclidean Spaces
definition
let M be locally_euclidean non empty TopSpace;
attr M is without_boundary means :Def5:
Int M = the carrier of M;
end;
notation
let M be locally_euclidean non empty TopSpace;
antonym M is with_boundary for M is without_boundary;
end;
Lm2: (M is locally_euclidean & for M1 be locally_euclidean non empty
TopSpace st M1=M holds M1 is without_boundary)
iff for p be Point of M ex U be a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
hereby
assume that
A1: M is locally_euclidean
and
A2: for M1 be locally_euclidean non empty TopSpace st M1=M holds
M1 is without_boundary;
let p be Point of M;
consider U be a_neighborhood of p,n such that
A3: M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A1;
set MU=M|U;
set TR=TOP-REAL n;
consider h be Function of MU,Tdisk(0.TR,1) such that
A4: h is being_homeomorphism by A3,T_0TOPSP:def 1;
A5: cl_Ball(0.TR,1) = Ball(0.TR,1) \/ Sphere(0.TR,1) by TOPREAL9:18;
A6: [#]Tdisk(0.TR,1) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider B=Ball(0.TR,1) as Subset of Tdisk(0.TR,1) by TOPREAL9:16;
A7: [#]MU = U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
A8: p in Int U by CONNSP_2:def 1;
reconsider B as open Subset of Tdisk(0.TR,1) by TSEP_1:9;
set HIB = B /\ h.:(Int U);
reconsider hib=HIB as Subset of TR by A6,XBOOLE_1:1;
A9: HIB c= Ball(0.TR,1) by XBOOLE_1:17;
IU is open by TSEP_1:9;
then h.:(Int U) is open by A4,TOPGRP_1:25;
then
A10: hib is open by TSEP_1:9,A9;
reconsider MM=M as locally_euclidean non empty TopSpace by A1;
A11: Int U c= U by TOPS_1:16;
A12: dom h = [#]MU by A4,TOPS_2:def 5;
then
A13: h.p in rng h by A8,A11,A7,FUNCT_1:def 3;
A14: h.p in Ball(0.TR,1)
proof
assume not h.p in Ball(0.TR,1);
then
A15: h.p in Sphere(0.TR,1) by A6,A13,A5,XBOOLE_0:def 3;
Fr MM = (the carrier of MM) \ Int MM by SUBSET_1:def 4
.= (the carrier of MM)\(the carrier of MM) by Def5,A2
.={} by XBOOLE_1:37;
hence contradiction by A15,A4,Th3;
end;
h.p in h.:(Int U) by A8,A11,A7,A12,FUNCT_1:def 6;
then h.p in hib by A14,XBOOLE_0:def 4;
then consider BB be ball Subset of TOP-REAL n such that
A16: BB c= hib
and
A17: h.p in BB by A10,MFOLD_1:3;
reconsider bb=BB as non empty Subset of Tdisk(0.TR,1)
by A16,A17,XBOOLE_1:1;
reconsider hb=h"bb as Subset of M by A7,XBOOLE_1:1;
bb is open by TSEP_1:9;
then
A18: h"bb is open by A4,TOPGRP_1:26;
A19: h"HIB c= h"(h.:Int U) by XBOOLE_1:17,RELAT_1:143;
AA: h"(h.:Int U) c= Int U by A4,FUNCT_1:82;
A21: M|hb = M|U | (h"bb) by A7,PRE_TOPC:7;
hb c= h"HIB by A16,RELAT_1:143;
then hb c= Int U by A19,AA;
then
A22: hb is open by A7,TSEP_1:9,A18,A11;
p in hb by A17, A8,A11,A7,A12,FUNCT_1:def 7;
then
A23: p in Int hb by A22,TOPS_1:23;
consider q be Point of TOP-REAL n, r be Real such that
A24: BB = Ball(q,r) by MFOLD_1:def 1;
rng h = [#]Tdisk(0.TR,1) by A4,TOPS_2:def 5;
then
A25: h.: (h"bb) = bb by FUNCT_1:77;
A26: TR|Ball(q,r) = Tball(q,r) by MFOLD_1:def 2;
A27: Tdisk(0.TR,1) | bb = TR|Ball(q,r) by A6, A24,PRE_TOPC:7;
then reconsider hh=h| (h"bb) as Function of M|hb,Tball(q,r)
by A21,JORDAN24:12,A25,A26;
reconsider hb as a_neighborhood of p by A23,CONNSP_2:def 1;
hh is being_homeomorphism by A4,A21,A25, A26,A27,METRIZTS:2;
then
A28: M|hb,Tball(q,r) are_homeomorphic by T_0TOPSP:def 1;
take hb;
take n;
A29: r>0 by A17,A24;
then Tball(q,r),Tball(0.TR,1) are_homeomorphic by MFOLD_1:9;
hence M|hb,Tball(0.TOP-REAL n,1) are_homeomorphic by A28,BORSUK_3:3,A29;
end;
assume
A30:for p be Point of M ex U being a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
thus M is locally_euclidean
proof
let p be Point of M;
consider U be a_neighborhood of p,n such that
A31: M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A30;
set En=Euclid n;
set TR=TOP-REAL n;
A32: Int U c= U by TOPS_1:16;
[#]Tdisk(0.TR,1) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider B=Ball(0.TR,1) as Subset of Tdisk(0.TR,1) by TOPREAL9:16;
set MU=M|U;
consider h be Function of MU,Tball(0.TOP-REAL n,1) such that
A33: h is being_homeomorphism by A31,T_0TOPSP:def 1;
N: n in NAT by ORDINAL1:def 12;
A34: Tball(0.TR,1) = TR|Ball(0.TR,1) by MFOLD_1:def 2;
then
A35: [#]Tball(0.TR,1) = Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider clB = cl_Ball(0.TR,1/2)
as non empty Subset of Tball(0.TR,1) by JORDAN:21,N;
A36: [#]MU = U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
reconsider hIU = h.:IU as Subset of TR by A35,XBOOLE_1:1;
A38: dom h = [#]MU by A33,TOPS_2:def 5;
then
A39: IU=h"hIU by A33,FUNCT_1:82,FUNCT_1:76;
A40: the TopStruct of TR = TopSpaceMetr En by EUCLID:def 8;
then reconsider hIUE=hIU as Subset of TopSpaceMetr En;
A41: p in Int U by CONNSP_2:def 1;
then
A42: h.p in hIU by A38,FUNCT_1:def 6;
then reconsider hp=h.p as Point of En by EUCLID:67;
reconsider Hp=h.p as Point of TR by A42;
IU is open by TSEP_1:9;
then h.:IU is open by A33,TOPGRP_1:25;
then hIU is open by A35,TSEP_1:9;
then hIU in the topology of TR by PRE_TOPC:def 2;
then consider r be Real such that
A43: r > 0
and
A44: Ball(hp,r) c= hIUE by A42,A40,PRE_TOPC:def 2,TOPMETR:15;
set r2=r/2;
A45: Ball(Hp,r)=Ball(hp,r) by TOPREAL9:13;
cl_Ball(Hp,r2) c= Ball(Hp,r) by N,XREAL_1:216,A43,JORDAN:21;
then
A46: cl_Ball(Hp,r2) c= hIU by A44,A45;
then reconsider CL=cl_Ball(Hp,r2) as Subset of Tball(0.TR,1)
by XBOOLE_1:1;
A47: cl_Ball(Hp,r2) c= [#]Tball(0.TR,1) by A46,XBOOLE_1:1;
then cl_Ball(Hp,r2) c= rng h by A33,TOPS_2:def 5;
then
A48: h.:(h"CL) = CL by FUNCT_1:77;
set r22=r2/2;
r22 < r2 by A43,XREAL_1:216;
then
A49: Ball(Hp,r22) c= Ball(Hp,r2) by N,JORDAN:18;
reconsider hCL=h"CL as Subset of M by A36,XBOOLE_1:1;
A50: (M|U) | (h"CL) = M| hCL by A36,PRE_TOPC:7;
A51: Ball(Hp,r2) c= cl_Ball(Hp,r2) by TOPREAL9:16;
then
A52: Ball(Hp,r22) c= cl_Ball(Hp,r2) by A49;
then reconsider BI = Ball(Hp,r22) as Subset of Tball(0.TR,1)
by A47,XBOOLE_1:1;
BI c= hIU by A46, A51,A49;
then
A53: h"BI c= h"hIU by RELAT_1:143;
reconsider hBI=h"BI as Subset of M by A36,XBOOLE_1:1;
BI is open by TSEP_1:9;
then h"BI is open by A33,TOPGRP_1:26;
then
A54: hBI is open by A39,A53,TSEP_1:9;
|.Hp - Hp.|=0 by TOPRNS_1:28;
then h.p in BI by A43;
then p in h"BI by A41,A32,A36,A38,FUNCT_1:def 7;
then p in Int hCL by A52,RELAT_1:143,TOPS_1:22,A54;
then reconsider hCL as a_neighborhood of p by CONNSP_2:def 1;
A55: Tball(0.TR,1) |CL = Tdisk(Hp,r2) by A34,A35,PRE_TOPC:7;
then reconsider hh=h| (h"CL) as Function of M|hCL,Tdisk(Hp,r2)
by A48,JORDAN24:12,A50;
hh is being_homeomorphism by A33,A55,METRIZTS:2,A48,A50;
then
A56: M|hCL,Tdisk(Hp,r2) are_homeomorphic by T_0TOPSP:def 1;
Tdisk(Hp,r2),Tdisk(0.TR,1) are_homeomorphic by Lm1, A43;
hence thesis by A56,BORSUK_3:3,A43;
end;
let M1 be locally_euclidean non empty TopSpace such that
A57: M1 = M;
thus Int M1 c= the carrier of M1;
let x be object;
assume x in the carrier of M1;
then reconsider p=x as Point of M1;
ex U being a_neighborhood of p,n st
M1|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A57,A30;
hence thesis by Def3;
end;
Lm3:
Tball(0.TOP-REAL n,1) is n-locally_euclidean &
for M1 be n-locally_euclidean non empty TopSpace st
M1 = Tball(0.TOP-REAL n,1) holds M1 is without_boundary
proof
set TR=TOP-REAL n;
set M=Tball(0.TR,1);
A1: for p be Point of M ex U be a_neighborhood of p st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
let p be Point of M;
Int [#]M = [#]M by TOPS_1:15;
then reconsider CM=[#]M as non empty a_neighborhood of p
by CONNSP_2:def 1;
take CM;
[#](M|CM)=CM by PRE_TOPC:def 5;
then reconsider cm=CM as non empty Subset of M|CM;
the TopStruct of M|CM,the TopStruct of M are_homeomorphic by TSEP_1:93;
hence thesis by TOPREALA:15;
end;
A2:for p be Point of M ex U be a_neighborhood of p,m st
M|U,Tball(0.TOP-REAL m,1) are_homeomorphic
proof
let p be Point of M;
ex U be a_neighborhood of p st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
by A1;
hence ex U be a_neighborhood of p,m st
M|U,Tball(0.TOP-REAL m,1) are_homeomorphic;
end;
then reconsider MM=M as locally_euclidean non empty TopSpace by Lm2;
MM is n-locally_euclidean
proof
let p be Point of MM;
consider U be a_neighborhood of p such that
A3: MM|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A1;
A: Tball(0.TOP-REAL n,1) = (TOP-REAL n) |Ball(0.TOP-REAL n,1)
by MFOLD_1:def 2;
A4: p in Int U by CONNSP_2:def 1;
consider W be a_neighborhood of p,m such that
A5: MM|W,Tdisk(0.TOP-REAL m,1) are_homeomorphic by Def1;
p in Int W by CONNSP_2:def 1;
then m=n by A4,XBOOLE_0:3,A3,A5,A,BROUWER3:15;
hence thesis by A5;
end;
hence M is n-locally_euclidean;
let M1 be n-locally_euclidean non empty TopSpace;
thus thesis by A2,Lm2;
end;
registration
let n;
cluster Tball(0.TOP-REAL n,1) -> n-locally_euclidean;
coherence by Lm3;
cluster Tball(0.TOP-REAL n,1) -> without_boundary;
coherence by Lm3;
end;
registration
let n be non zero Nat;
cluster Tdisk(0.TOP-REAL n,1) -> with_boundary;
coherence
proof
set TR=TOP-REAL n;
set M=Tdisk(0.TR,1);
reconsider CM=[#]M as non empty Subset of M;
consider p be object such that
A1: p in Sphere(0.TR,1) by XBOOLE_0:def 1;
reconsider p as Point of TR by A1;
A2: [#]M=cl_Ball(0.TR,1) by PRE_TOPC:def 5;
Sphere(0.TR,1) c= cl_Ball(0.TR,1) by TOPREAL9:17;
then reconsider pp=p as Point of M by A2,A1;
A3: Fr cl_Ball(0.TR,1) = Sphere(0.TR,1) by BROUWER2:5;
[#](M|CM)=CM by PRE_TOPC:def 5;
then reconsider cm=CM as non empty Subset of M|CM;
Int [#]M = [#]M by TOPS_1:15;
then reconsider CM as non empty a_neighborhood of pp by CONNSP_2:def 1;
A4: M|CM= M by TSEP_1:3;
Ball(0.TR,1) c= Int cl_Ball(0.TR,1) by TOPREAL9:16,TOPS_1:24;
then cl_Ball(0.TR,1) is non boundary compact;
then consider h be Function of M|CM,M such that
A5: h is being_homeomorphism
and
A6: h.:Fr cl_Ball(0.TR,1) = Fr cl_Ball(0.TR,1) by BROUWER2:7,A4;
dom h = [#]M by A5,A4,TOPS_2:def 5;
then
A7:h.pp in h.:Sphere(0.TR,1) by A1,FUNCT_1:def 6;
M is with_boundary
proof
assume
A8: M is without_boundary;
Fr M = (the carrier of M)\(the carrier of M) by A8,SUBSET_1:def 4
.={} by XBOOLE_1:37;
hence thesis by A3,A6,A7,A5,Th3;
end;
hence thesis;
end;
end;
registration
let n;
cluster without_boundary for n-locally_euclidean non empty TopSpace;
existence
proof
take M=Tball(0.TOP-REAL n,1);
thus thesis;
end;
end;
registration
let n be non zero Nat;
cluster with_boundary compact for n-locally_euclidean non empty TopSpace;
existence
proof
take M=Tdisk(0.TOP-REAL n,1);
thus thesis;
end;
end;
registration
let M be without_boundary locally_euclidean non empty TopSpace;
cluster Fr M -> empty;
coherence
proof
Fr M = (the carrier of M) \ Int M by SUBSET_1:def 4
.= (the carrier of M)\(the carrier of M) by Def5
.={} by XBOOLE_1:37;
hence thesis;
end;
end;
registration
let M be with_boundary locally_euclidean non empty TopSpace;
cluster Fr M -> non empty;
coherence
proof
assume Fr M is empty;
then {} = (the carrier of M) \ Int M by SUBSET_1:def 4;
then (the carrier of M) c= Int M by XBOOLE_1:37;
hence thesis by XBOOLE_0:def 10,Def5;
end;
end;
registration
let n be zero Nat;
cluster -> without_boundary for n-locally_euclidean non empty TopSpace;
coherence
proof
set TR=TOP-REAL n,S=Sphere(0.TR,1);
let M be n-locally_euclidean non empty TopSpace;
assume M is with_boundary;
then consider p be object such that
A1: p in Fr M by XBOOLE_0:def 1;
reconsider p as Point of M by A1;
consider U be a_neighborhood of p, m be Nat, h be Function of M|U,
Tdisk(0.TOP-REAL m,1) such that
A2: h is being_homeomorphism
and
A3: h.p in Sphere(0.TOP-REAL m,1) by A1, Th3;
A4: p in Int U by CONNSP_2:def 1;
consider W be a_neighborhood of p such that
A5: M|W,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
A6: p in Int W by CONNSP_2:def 1;
M|U,Tdisk(0.TOP-REAL m,1) are_homeomorphic by A2,T_0TOPSP:def 1;
then reconsider hp=h.p as Point of TR
by A3,A6,A4,XBOOLE_0:3,BROUWER3:14,A5;
hp = 0.TR by A3;
then |. 0.TR .| = 1 by A3,TOPREAL9:12;
hence thesis;
end;
end;
:: Correspondence between Classical and Extended Concepts
:: of Locally Euclidean Spaces
theorem
M is without_boundary locally_euclidean non empty TopSpace
iff
for p be Point of M
ex U be a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
thus M is without_boundary locally_euclidean non empty TopSpace implies
for p be Point of M ex U be a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
assume
A1: M is without_boundary locally_euclidean non empty TopSpace;
then for M1 be locally_euclidean non empty TopSpace st M1=M holds
M1 is without_boundary;
hence thesis by A1,Lm2;
end;
thus thesis by Lm2;
end;
theorem Th5:
for M be with_boundary locally_euclidean non empty TopSpace
for p be Point of M, n st
ex U be a_neighborhood of p st
M|U,Tdisk(0.TOP-REAL (n+1),1) are_homeomorphic
holds
for pF be Point of M|Fr M st p=pF
ex U being a_neighborhood of pF st
(M|Fr M) |U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
let M be with_boundary locally_euclidean non empty TopSpace;
let p be Point of M, n such that
A1: ex U be a_neighborhood of p st
M|U,Tdisk(0.TOP-REAL (n+1),1) are_homeomorphic;
set n1=n+1;
set TR=TOP-REAL n1;
consider W be a_neighborhood of p such that
A2: M|W,Tdisk(0.TR,1) are_homeomorphic by A1;
A3: p in Int W by CONNSP_2:def 1;
set TR1 = TOP-REAL n;
set CL=cl_Ball(0.TR,1);
set S=Sphere(0.TR,1);
set F=Fr M,MF=M|F;
let pF be Point of MF such that
A4: p=pF;
A5:[#]MF=F by PRE_TOPC:def 5;
then consider U be a_neighborhood of p,m be Nat, h be Function of
M|U,Tdisk(0.TOP-REAL m,1) such that
A6: h is being_homeomorphism
and
A7: h.p in Sphere(0.TOP-REAL m,1) by A4, Th3;
A8: p in Int U by CONNSP_2:def 1;
M|U,Tdisk(0.TOP-REAL m,1) are_homeomorphic by A6,T_0TOPSP:def 1;
then
A9:m=n+1 by A3,A8,XBOOLE_0:3,A2, BROUWER3:14;
then reconsider h as Function of M|U,Tdisk(0.TR,1);
A10: Int U c= U by TOPS_1:16;
[#](M|U)=U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
set MU=M|U;
A11:pF in Int U by A4, CONNSP_2:def 1;
then p in F/\IU by A4,A5,XBOOLE_0:def 4;
then reconsider FIU=F/\(Int U) as non empty Subset of MU;
A12: [#](M|U)=U by PRE_TOPC:def 5;
IU is open by TSEP_1:9;
then h .: IU is open by A9,A6,TOPGRP_1:25;
then h .: IU in the topology of Tdisk(0.TR,1) by PRE_TOPC:def 2;
then consider W be Subset of TR such that
A13: W in the topology of TR
and
A14: h .: IU = W/\ [#]Tdisk(0.TR,1) by PRE_TOPC:def 4;
reconsider W as open Subset of TR by A13,PRE_TOPC:def 2;
A15: h .: IU = W/\CL by PRE_TOPC:def 5,A14;
A16: dom h =[#](M|U) by A6, TOPS_2:def 5;
then
A17: h.p in h.:IU by A4,A11,FUNCT_1:def 6;
then reconsider hp=h.p as Point of TR by A15;
A18: Int W=W by TOPS_1:23;
A19: |. hp - 0.TR.| =1 by A9, A7,TOPREAL9:9;
reconsider HP=hp as Point of Euclid n1 by EUCLID:67;
h.p in W by A17,A14,XBOOLE_0:def 4;
then consider s be Real such that
A20: s>0
and
A21: Ball(HP,s) c= W by A18,GOBOARD6:5;
set s2=s/2,m=min(s/2,1/2);
set V0 = S /\ Ball(hp,m);
set hV0=h"V0;
A22: m<=s2 by XXREAL_0:17;
s2 < s by A20,XREAL_1:216;
then
A23:Ball(hp,m) c= Ball(hp,s) by A22,XXREAL_0:2,JORDAN:18;
A24:Ball(HP,s)=Ball(hp,s) by TOPREAL9:13;
A25: hV0 c= F
proof
let x be object;
assume
A26: x in hV0;
then
A27: h.x in V0 by FUNCT_1:def 7;
A28:x in dom h by A26,FUNCT_1:def 7;
then reconsider q=x as Point of M by A16,A12;
reconsider hq=h.q as Point of TR by A27;
h.q in Ball(hp,m) by A27,XBOOLE_0:def 4;
then
A29: h.q in Ball(hp,s) by A23;
A30: h.q in Sphere(0.TR,1) by A27,XBOOLE_0:def 4;
then |. hq -0.TR .| = 1 by TOPREAL9:9;
then hq in CL;
then h.q in h.:IU by A15, A29,A21,A24,XBOOLE_0:def 4;
then consider y be object such that
A31: y in dom h
and
A32: y in IU
and
A33: h.y=h.q by FUNCT_1:def 6;
y=q by A6,A31,A33,A28,FUNCT_1:def 4;
then U is a_neighborhood of q by A32,CONNSP_2:def 1;
hence thesis by A9,A6,Th3,A30;
end;
reconsider FIU1=FIU as Subset of MF by XBOOLE_1:17,A5;
Int U in the topology of M by PRE_TOPC:def 2;
then FIU1 in the topology of M|F by A5,PRE_TOPC:def 4;
then
A34: FIU1 is open by PRE_TOPC:def 2;
A35: MF|FIU1 = M| (Fr M /\Int U) by XBOOLE_1:17,PRE_TOPC:7;
set Mfiu=MU|FIU;
A36: F/\U c= U by XBOOLE_1:17;
A38:[#] (TR|CL) = CL by PRE_TOPC:def 5;
then reconsider hFIU=h.:FIU as Subset of TR by XBOOLE_1:1;
A39:[#](TR|hFIU)=hFIU by PRE_TOPC:def 5;
A40:Tdisk(0.TR,1) | (h.:FIU) = TR|hFIU by A38,PRE_TOPC:7;
then reconsider hfiu=h|FIU as Function of Mfiu, TR|hFIU by JORDAN24:12;
A41: hfiu is being_homeomorphism by A9,A6,METRIZTS:2,A40;
A42:Ball(0.TR1,1) misses Sphere(0.TR1,1) by TOPREAL9:19;
A43: S c= CL by TOPREAL9:17;
A44: IU = h"(h.:IU) by FUNCT_1:82,A6,FUNCT_1:76,A16;
V0 c= Ball(hp,m) by XBOOLE_1:17;
then
A45: V0 c= W by A21,A23,A24;
BB: V0 c= hFIU
proof
let x be object;
assume
A46: x in S/\ Ball(hp,m);
then reconsider q=x as Point of TR;
q in S by A46,XBOOLE_0:def 4;
then q in h.:IU by A45,A46,A15,A43,XBOOLE_0:def 4;
then consider w be object such that
A47: w in dom h
and
A48: w in IU
and
A49: h.w = q by FUNCT_1:def 6;
reconsider w as Point of MU by A47;
w in hV0 by A46,A47,A49,FUNCT_1:def 7;
then w in FIU by A25,A48,XBOOLE_0:def 4;
hence thesis by A47,A49,FUNCT_1:def 6;
end;
A51: V0 c= S by XBOOLE_1:17;
then V0 c= CL by A43;
then V0 c= h.:IU by A45,A14,XBOOLE_1:19, A38;
then
A52: hV0 c= IU by A44,RELAT_1:143;
A53: rng h = [#]Tdisk(0.TR,1) by A9,A6, TOPS_2:def 5;
then h.:(h"V0) = V0 by FUNCT_1:77, A43,A51,XBOOLE_1:1,A38;
then
A54: Tdisk(0.TR,1) | (h.:(h"V0)) = TR |V0 by PRE_TOPC:7,A43,A51,XBOOLE_1:1;
A55:CL=S\/Ball(0.TR,1) by TOPREAL9:18;
A56: hFIU /\ Ball(hp,m) c= V0
proof
let x be object;
assume
A57: x in hFIU /\ Ball(hp,m);
then reconsider q=x as Point of TR;
A58: x in hFIU by A57,XBOOLE_0:def 4;
A59: q in S
proof
reconsider Q=q as Point of Euclid n1 by EUCLID:67;
set WB=W/\Ball(0.TR,1);
A60: Int WB=WB by TOPS_1:23;
hFIU c= h.:IU by XBOOLE_1:17,RELAT_1:123;
then
A61: q in W by A58,A14,XBOOLE_0:def 4;
assume not q in S;
then q in Ball(0.TR,1) by A58, A38,A55,XBOOLE_0:def 3;
then q in WB by A61,XBOOLE_0:def 4;
then consider w be Real such that
A62: w>0
and
A63: Ball(Q,w) c= WB by A60,GOBOARD6:5;
set B=Ball(q,w);
A64: Ball(Q,w)=Ball(q,w) by TOPREAL9:13;
consider u be object such that
A65: u in dom h
and
A66: u in FIU
and
A67: h.u=q by FUNCT_1:def 6,A58;
reconsider u as Point of M by A66;
A68: Ball(0.TR,1) c= CL by A55, XBOOLE_1:11;
WB c= Ball(0.TR,1) by XBOOLE_1:17;
then
A69: B c= Ball(0.TR,1) by A63,A64;
then reconsider BB=B as Subset of Tdisk(0.TR,1) by A68,XBOOLE_1:1,A38;
reconsider hBB=h"BB as Subset of M by A12,XBOOLE_1:1;
A70: B in the topology of TR by PRE_TOPC:def 2;
|.q-q.|=0 by TOPRNS_1:28;
then q in BB by A62;
then
A71: u in hBB by A65,A67,FUNCT_1:def 7;
A72: TR|Ball(q,w) = Tball(q,w) by MFOLD_1:def 2;
BB /\CL =BB by A68,XBOOLE_1:1,A69,XBOOLE_1:28;
then BB in the topology of Tdisk(0.TR,1) by A70,A38,PRE_TOPC:def 4;
then BB is open by PRE_TOPC:def 2;
then
A73: h"BB is open by TOPGRP_1:26,A9,A6;
WB c= W by XBOOLE_1:17;
then BB c= W by A63,A64;
then BB c= h.:IU by XBOOLE_1:19,A14;
then h"BB c= Int U by RELAT_1:143,A44;
then hBB is open by A10,A12,A73,TSEP_1:9;
then
A74: Int hBB = hBB by TOPS_1:23;
A75: Tdisk(0.TR,1) | BB = TR|Ball(q,w) by A38,PRE_TOPC: 7;
reconsider hBB as a_neighborhood of u by A74,A71,CONNSP_2:def 1;
A76: h.:hBB =BB by FUNCT_1:77,A53;
A77: MU|h"BB = M|hBB by A12,PRE_TOPC:7;
then
reconsider hB=h|hBB as Function of M|hBB, TR|Ball(q,w)
by JORDAN24:12,A75,A76;
hB is being_homeomorphism by A9,A6,A75,A76,A77,METRIZTS:2;
then
A78: M|hBB,Tball(q,w) are_homeomorphic by A72,T_0TOPSP:def 1;
Tball(q,w),Tball(0.TR,1) are_homeomorphic by A62,MFOLD_1:9;
then M|hBB,Tball(0.TR,1) are_homeomorphic by A78,A62,BORSUK_3:3;
then
A79: u in Int M by Def3;
u in F by A66,XBOOLE_0:def 4;
then u in [#]M \ Int M by SUBSET_1:def 4;
hence thesis by XBOOLE_0:def 5,A79;
end;
x in Ball(hp,m) by A57,XBOOLE_0:def 4;
hence thesis by A59,XBOOLE_0:def 4;
end;
S/\ Ball(hp,m)/\Ball(hp,m) = S/\ (Ball(hp,m)/\Ball(hp,m)) by XBOOLE_1:16
.= V0;
then
A80: hFIU /\ Ball(hp,m) = V0 by A56,XBOOLE_1:26,BB;
reconsider v0=V0 as Subset of TR|hFIU by A39,BB;
Ball(hp,m) in the topology of TR by PRE_TOPC:def 2;
then v0 in the topology of TR|hFIU by A80,PRE_TOPC:def 4,A39;
then
A81: v0 is open by PRE_TOPC:def 2;
A82:Ball(0.TR1,1) \/ Sphere(0.TR1,1) = cl_Ball(0.TR1,1) by TOPREAL9:18;
A83:Tball(0.TR1,1) = TR1|Ball(0.TR1,1) by MFOLD_1:def 2;
A84: |. hp - 0.TR.| = |. 0.TR - hp.| by TOPRNS_1:27;
A85:m>0 by A20,XXREAL_0:21;
then
A86: |.0.TR - hp.| < 1+m by A19,A84,XREAL_1:29;
|.hp-hp.|=0 by TOPRNS_1:28;
then hp in Ball(hp,m) by A85;
then
A87:hp in V0 by A9,A7,XBOOLE_0:def 4;
A88: pF in Int U by A4,CONNSP_2:def 1;
then
A89: pF in hV0 by A16,A10,A12,A4,A87,FUNCT_1:def 7;
m <= 1/2 by XXREAL_0:17;
then m < |.0.TR - hp.| by A19,A84,XXREAL_0:2;
then
consider g be Function of TR | (S /\ cl_Ball(hp,m)),Tdisk(0.TR1,1) such that
A90: g is being_homeomorphism
and
A91: g.:(S /\ Sphere(hp,m)) = Sphere(0. TR1,1) by A19,A84,A86,BROUWER3:19;
A92:(g.:S) /\ (g.:Ball(hp,m)) = g.:V0 by A90,FUNCT_1:62;
A93: [#]Mfiu = FIU by PRE_TOPC:def 5;
then reconsider U0=hV0 as non empty Subset of Mfiu
by A52,A25,XBOOLE_1:19,A16,A88,A4,A87,FUNCT_1:def 7;
reconsider U0 = hV0 as Subset of Mfiu by A52,A25,XBOOLE_1:19,A93;
A94:[#](MF|FIU1)=FIU by PRE_TOPC:def 5;
then reconsider u0=U0 as Subset of MF|FIU1 by A93;
hfiu"v0 = FIU /\ U0 by FUNCT_1:70;
then hfiu"v0 = U0 by A52,A25,XBOOLE_1:19,XBOOLE_1:28;
then
A95: U0 is open by A81,A41,TOPGRP_1:26;
reconsider FV0=u0 as Subset of MF by XBOOLE_1:1,A93;
A96: F/\(Int U) c= F/\U by XBOOLE_1:26,TOPS_1:16;
then Mfiu = M| (Fr M /\Int U) by A36,XBOOLE_1:1,PRE_TOPC:7;
then FV0 is open by A34,A35,A95,TSEP_1:9,A94;
then pF in Int FV0 by A89,TOPS_1:22;
then reconsider FV0 as a_neighborhood of pF by CONNSP_2:def 1;
reconsider MV0=FV0 as Subset of M by A52,XBOOLE_1:1;
hV0 c= IU/\F by A52,A25,XBOOLE_1:19;
then FV0 c= F/\U by A96;
then
A97:MU | (h"V0) = M|MV0 by PRE_TOPC:7,A36,XBOOLE_1:1;
(S/\Sphere(hp,m)) misses V0 by TOPREAL9:19,XBOOLE_1:76;
then
A98:Sphere(0. TOP-REAL n,1) misses g.:V0 by A90,A91,FUNCT_1:66;
A99:((g.:S) /\ (g.:Sphere(hp,m))) = g.:(S/\Sphere(hp,m)) by A90,FUNCT_1:62;
A100: [#](TR| (S /\ cl_Ball(hp,m))) = S /\ cl_Ball(hp,m) by PRE_TOPC:def 5;
then
A101: dom g = S /\ cl_Ball(hp,m) by A90,TOPS_2:def 5;
A102: Ball(hp,m) \/ Sphere(hp,m) = cl_Ball(hp,m) by TOPREAL9:18;
then reconsider ZV0=V0 as Subset of TR | (S /\ cl_Ball(hp,m))
by XBOOLE_1:7,26,A100;
A103: g.:cl_Ball(hp,m) = (g.:Ball(hp,m)) \/ (g.:Sphere(hp,m))
by A102,RELAT_1:120;
A104: [#](Tdisk(0.TR1,1)) = cl_Ball(0.TR1,1) by PRE_TOPC:def 5;
then rng g = cl_Ball(0.TR1,1) by A90,TOPS_2:def 5;
then cl_Ball(0.TR1,1) = g.:(S /\ cl_Ball(hp,m)) by A101,RELAT_1:113
.= (g.:S) /\ (g.:cl_Ball(hp,m)) by A90,FUNCT_1:62
.= (g.:V0) \/ Sphere(0.TOP-REAL n,1)
by A103,A99,A92,A91,XBOOLE_1:23;
then g.:V0 = Ball(0.TR1,1) by A82,A42,A98,XBOOLE_1:71;
then
A105: Tdisk(0.TR1,1) | (g.:ZV0) = Tball(0.TR1,1) by PRE_TOPC:7,A83,A104;
A106:TR | (S /\ cl_Ball(hp,m)) | ZV0 = TR|V0 by A100,PRE_TOPC:7;
then reconsider GG=g|ZV0 as Function of TR | V0,Tball(0.TR1,1)
by A87,JORDAN24:12,A105;
A107: GG is being_homeomorphism by A90,METRIZTS:2,A106,A105;
A108: M|MV0 = MF|FV0 by A5,PRE_TOPC:7;
then reconsider HH=h|FV0 as Function of MF|FV0,TR|V0
by A97,A54,JORDAN24:12;
reconsider GH=GG*HH as Function of MF |FV0,Tball(0.TR1,1) by A87;
take FV0;
HH is being_homeomorphism by A9,A6,METRIZTS:2,A97,A54,A108;
then GH is being_homeomorphism by A87,A107,TOPS_2:57;
hence thesis by T_0TOPSP:def 1;
end;
Lm4:for M be locally_euclidean non empty TopSpace
for p be Point of M|Int M
ex U be a_neighborhood of p,n st
(M|Int M) |U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
let M be locally_euclidean non empty TopSpace;
set MI=M|Int M;
let p be Point of M|Int M;
A1: [#] MI = Int M by PRE_TOPC:def 5;
then p in Int M;
then reconsider q=p as Point of M;
consider U be a_neighborhood of q, n such that
A2: M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A1,Def3;
A3: Int U c= U by TOPS_1:16;
A4: Int M /\ Int U in the topology of M by PRE_TOPC:def 2;
A5: Int U c= U by TOPS_1:16;
set MU=M|U,TR=TOP-REAL n;
consider h be Function of MU,Tball(0.TR,1) such that
A6: h is being_homeomorphism by A2,T_0TOPSP:def 1;
A7: [#]MU = U by PRE_TOPC:def 5;
Int U /\ Int M c= Int U by XBOOLE_1:17;
then reconsider UIM = Int M /\ Int U as Subset of MU by A5,A7,XBOOLE_1:1;
A8: dom h =[#]MU by A6,TOPS_2:def 5;
A10:Tball(0.TR,1) = TR|Ball(0.TR,1) by MFOLD_1:def 2;
then
A11: [#]Tball(0.TR,1) = Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider hum=h.:UIM as Subset of TR by XBOOLE_1:1;
UIM /\[#]MU = UIM by XBOOLE_1:28;
then UIM in the topology of MU by A4,PRE_TOPC:def 4;
then UIM is open by PRE_TOPC:def 2;
then h.:UIM is open by A6,TOPGRP_1:25;
then hum is open by TSEP_1:9,A11;
then
A12: Int hum = hum by TOPS_1:23;
A13: h"(h.:UIM) c= UIM by A6,FUNCT_1:82;
A14: q in Int U by CONNSP_2:def 1;
then
A15: q in UIM by A1,XBOOLE_0:def 4;
then h.q in hum by A8,FUNCT_1:def 6;
then reconsider hq=h.q as Point of TR;
reconsider HQ=hq as Point of Euclid n by EUCLID:67;
h.q in h.:UIM by A15,A8,FUNCT_1:def 6;
then consider s be Real such that
A16: s>0
and
A17: Ball(HQ,s) c= hum by A12,GOBOARD6:5;
A18:Ball(HQ,s)=Ball(hq,s) by TOPREAL9:13;
then reconsider BB=Ball(hq,s) as Subset of Tball(0.TR,1) by A17,XBOOLE_1:1;
BB is open by TSEP_1:9;
then reconsider hBB=h"BB as open Subset of MU by A6,TOPGRP_1:26;
hBB c= h"(h.:UIM) by A17,A18,RELAT_1:143;
then
A19: hBB c= UIM by A13;
reconsider hBBM=hBB as Subset of M by A7,XBOOLE_1:1;
Int U /\ Int M c= Int M by XBOOLE_1:17;
then reconsider HBB=hBBM as Subset of MI by A19,XBOOLE_1:1,A1;
hBBM is open by TSEP_1:9,A19;
then
A20:HBB is open by TSEP_1:9;
A21: M|hBBM = MI|HBB by A1,PRE_TOPC:7;
rng h = [#]Tball(0.TR,1) by A6,TOPS_2:def 5;
then h.:hBB=BB by FUNCT_1:77;
then
A22:Tball(0.TR,1) | (h.:hBB) = TR|Ball(hq,s) by A10,A11,PRE_TOPC:7;
|.hq-hq.|=0 by TOPRNS_1:28;
then hq in BB by A16;
then p in HBB by FUNCT_1:def 7,A14,A3,A8,A7;
then p in Int HBB by A20,TOPS_1:23;
then reconsider HBB as a_neighborhood of p by CONNSP_2:def 1;
A23: MU|hBB =M|hBBM by A7,PRE_TOPC:7;
then reconsider hh=h|hBB as Function of MI|HBB,TR|Ball(hq,s)
by A22,JORDAN24:12,A21;
hh is being_homeomorphism by A6,A22,A23,A21,METRIZTS:2;
then MI|HBB,TR|Ball(hq,s) are_homeomorphic by T_0TOPSP:def 1;
then
A24: MI|HBB,Tball(hq,s) are_homeomorphic by MFOLD_1:def 2;
take HBB;
Tball(hq,s),Tball(0.TR,1) are_homeomorphic by A16,MFOLD_1:9;
hence thesis by A16,A24,BORSUK_3:3;
end;
registration
let M be locally_euclidean non empty TopSpace;
cluster M|Int M -> locally_euclidean;
coherence
proof
for p be Point of (M|Int M) ex U be a_neighborhood of p,n st
(M|Int M) |U,Tball(0.TOP-REAL n,1) are_homeomorphic by Lm4;
hence thesis by Lm2;
end;
cluster M|Int M -> without_boundary;
coherence
proof
for p be Point of (M|Int M) ex U be a_neighborhood of p,n st
(M|Int M) |U,Tball(0.TOP-REAL n,1) are_homeomorphic by Lm4;
hence thesis by Lm2;
end;
end;
Lm5:
for M be with_boundary locally_euclidean non empty TopSpace
for p be Point of M
for pM be Point of M|Fr M st p=pM
for U be a_neighborhood of p,n be Nat,h
be Function of M|U,Tdisk(0.TOP-REAL n,1)
st h is being_homeomorphism & h.p in Sphere(0.TOP-REAL n,1)
ex n1 be Nat,U be a_neighborhood of pM st n1+1=n &
(M|Fr M) |U,Tball(0.TOP-REAL n1,1) are_homeomorphic
proof
let M be with_boundary locally_euclidean non empty TopSpace;
let p be Point of M;
let pM be Point of M|Fr M such that
A1:p=pM;
let U be a_neighborhood of p;
let n be Nat;
let h be Function of M|U,Tdisk(0.TOP-REAL n,1) such that
A2: h is being_homeomorphism
and
A3: h.p in Sphere(0.TOP-REAL n,1);
set TR=TOP-REAL n;
n>0
proof
assume n<=0;
then n =0;
then h.p = 0.TR by A3,JORDAN2C:105;
then |. 0.TR .| = 1 by A3,TOPREAL9:12;
hence thesis by EUCLID_2:42;
end;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
take n1;
M|U,Tdisk(0.TOP-REAL (n1+1),1) are_homeomorphic by A2,T_0TOPSP:def 1;
then ex U be a_neighborhood of pM st (M|Fr M) |U,Tball(0.TOP-REAL n1,1)
are_homeomorphic by Th5,A1;
hence thesis;
end;
registration
let M be with_boundary locally_euclidean non empty TopSpace;
cluster M|Fr M -> locally_euclidean;
coherence
proof
set MF=M|Fr M;
now
let pM be Point of MF;
A1: [#]MF=Fr M by PRE_TOPC:def 5;
then pM in Fr M;
then reconsider p=pM as Point of M;
consider U be a_neighborhood of p,n be Nat, h be Function of
M|U, Tdisk(0.TOP-REAL n,1) such that
A2: h is being_homeomorphism
and
A3: h.p in Sphere(0.TOP-REAL n,1) by Th3, A1;
ex n1 be Nat,U be a_neighborhood of pM st n1+1=n &
(M|Fr M) |U,Tball(0.TOP-REAL n1,1) are_homeomorphic by Lm5,A2,A3;
hence ex U be a_neighborhood of pM,n1 be Nat st
(M|Fr M) |U,Tball(0.TOP-REAL n1,1) are_homeomorphic;
end;
hence thesis by Lm2;
end;
cluster M|Fr M -> without_boundary;
coherence
proof
set MF=M|Fr M;
now
let pM be Point of MF;
A4: [#]MF=Fr M by PRE_TOPC:def 5;
then pM in Fr M;
then reconsider p=pM as Point of M;
consider U be a_neighborhood of p,n be Nat, h be Function of
M|U, Tdisk(0.TOP-REAL n,1) such that
A5: h is being_homeomorphism
and
A6: h.p in Sphere(0.TOP-REAL n,1) by Th3,A4;
ex n1 be Nat,U be a_neighborhood of pM st n1+1=n &
(M|Fr M) |U,Tball(0.TOP-REAL n1,1) are_homeomorphic by Lm5,A5,A6;
hence ex U be a_neighborhood of pM,n1 be Nat st (M|Fr M) |U,
Tball(0.TOP-REAL n1,1) are_homeomorphic;
end;
hence thesis by Lm2;
end;
end;
begin :: Cartesian Product of Locally Euclidean Spaces
registration
let N,M be locally_euclidean non empty TopSpace;
cluster [:N,M:] -> locally_euclidean;
coherence
proof
let p be Point of [:N,M:];
p in the carrier of [:N,M:];
then p in [:the carrier of N,the carrier of M:] by BORSUK_1:def 2;
then consider x,y be object such that
A1: x in the carrier of N and
A2: y in the carrier of M and
A3: p=[x,y] by ZFMISC_1: def 2;
reconsider x as Point of N by A1;
consider Ux be a_neighborhood of x, n such that
A4: N|Ux,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def1;
reconsider y as Point of M by A2;
consider Uy be a_neighborhood of y, m such that
A5: M|Uy,Tdisk(0.TOP-REAL m,1) are_homeomorphic by Def1;
consider hy be Function of M|Uy,Tdisk(0.TOP-REAL m,1) such that
A6: hy is being_homeomorphism by A5,T_0TOPSP:def 1;
consider hx be Function of N|Ux,Tdisk(0.TOP-REAL n,1) such that
A7:hx is being_homeomorphism by A4,T_0TOPSP:def 1;
[:hx,hy:] is being_homeomorphism by A6,TIETZE_2:15,A7;
then
A8: [:N|Ux,M|Uy:],[:Tdisk(0.TOP-REAL n,1),Tdisk(0.TOP-REAL m,1):]
are_homeomorphic by T_0TOPSP:def 1;
reconsider mn=m+n as Nat;
ex hf be Function of [: Tdisk( 0.TOP-REAL n,1),Tdisk( 0.TOP-REAL m,1):],
Tdisk(0.TOP-REAL mn,1) st hf is being_homeomorphism &
hf.:[:Ball(0.TOP-REAL n,1), Ball(0.TOP-REAL m,1):] =
Ball(0. TOP-REAL mn,1) by TIETZE_2:19;
then
A9: [:Tdisk( 0.TOP-REAL n,1),Tdisk( 0.TOP-REAL m,1):],
Tdisk(0.TOP-REAL mn,1) are_homeomorphic
by T_0TOPSP:def 1;
[:N|Ux,M|Uy:] = [:N,M:] | [:Ux,Uy:] by BORSUK_3:22;
hence thesis by A9,A8,BORSUK_3:3,A3;
end;
end;
theorem Th6:
for N,M be locally_euclidean non empty TopSpace holds
Int [:N,M:] = [:Int N,Int M:]
proof
let N,M be locally_euclidean non empty TopSpace;
set NM=[:N,M:],IN=Int N,IM=Int M;
thus Int NM c= [:IN,IM:]
proof
let z be object;
assume
A1: z in Int NM;
then reconsider p=z as Point of NM;
z in the carrier of NM by A1;
then z in [:the carrier of N,the carrier of M:] by BORSUK_1:def 2;
then consider x,y be object such that
A2: x in the carrier of N and
A3: y in the carrier of M and
A4: z=[x,y] by ZFMISC_1: def 2;
reconsider y as Point of M by A3;
reconsider x as Point of N by A2;
assume
A5: not z in [:IN,IM:];
per cases by A5,A4,ZFMISC_1:87;
suppose
A6: not x in IN;
consider W be a_neighborhood of y,m be Nat such that
A7: M|W,Tdisk(0.TOP-REAL m,1) are_homeomorphic by Def1;
x in [#]N\IN by A6,XBOOLE_0:def 5;
then x in Fr N by SUBSET_1:def 4;
then consider U be a_neighborhood of x,n be Nat, h be Function of
N|U,Tdisk(0.TOP-REAL n,1) such that
A8: h is being_homeomorphism
and
A9: h.x in Sphere(0.TOP-REAL n,1) by Th3;
A10: y in Int W by CONNSP_2:def 1;
reconsider mn=m+n as Nat;
set TRm=TOP-REAL m,TRn=TOP-REAL n,TRnm=TOP-REAL mn;
consider f be Function of M|W,Tdisk(0.TRm,1) such that
A11: f is being_homeomorphism by A7,T_0TOPSP:def 1;
A12: not h.x in Ball(0.TRn,1) by TOPREAL9:19,A9,XBOOLE_0:3;
consider hf be Function of [: Tdisk(0.TRn,1),Tdisk( 0.TRm,1):],
Tdisk(0.TRnm,1) such that
A13: hf is being_homeomorphism
and
A14: hf.:[:Ball(0.TRn,1), Ball(0.TRm,1):] = Ball(0.TRnm,1) by TIETZE_2:19;
set H=hf*[:h,f:];
[:h,f:] is being_homeomorphism by A8,A11,TIETZE_2:15;
then
A15: H is being_homeomorphism by A13,TOPS_2:57;
then
A16: rng H = [#]Tdisk(0.TRnm,1) by TOPS_2:def 5;
A17: Int W c= W by TOPS_1:16;
A18: Int U c= U by TOPS_1:16;
x in Int U by CONNSP_2:def 1;
then
A19: [x,y] in [:U,W:] by A18,A17,A10,ZFMISC_1:87;
n+m in NAT by ORDINAL1:def 12;
then
A20: [#]Tdisk(0.TRnm,1) = cl_Ball(0.TRnm,1) by BROUWER:3;
A21: [:N|U,M|W:] = NM| [:U,W:] by BORSUK_3:22;
then dom H = [#](NM| [:U,W:]) by A15,TOPS_2:def 5;
then
A22: p in dom H by A19,A4,PRE_TOPC:def 5;
then
A23: [:h,f:].p in dom hf by FUNCT_1:11;
dom [:h,f:] = [:dom h,dom f:] by FUNCT_3:def 8;
then
SS: [:h,f:].(x,y) = [h.x,f.y] by A22,FUNCT_1:11,A4,FUNCT_3:65;
A25: H.p = hf.([:h,f:].p) by A22,FUNCT_1:12;
H.p in Sphere(0.TRnm,1)
proof
H.p in cl_Ball(0.TRnm,1) by A16,A20,A22,FUNCT_1:def 3;
then
A26: H.p in Sphere(0.TRnm,1)\/Ball(0.TRnm,1) by TOPREAL9:18;
assume not H.p in Sphere(0.TRnm,1);
then H.p in hf.:[:Ball(0.TRn,1), Ball(0.TRm,1):]
by A26,XBOOLE_0:def 3,A14;
then consider w be object such that
A27: w in dom hf
and
A28: w in [:Ball(0.TRn,1), Ball(0.TRm,1):]
and
A29: hf.w =H.p by FUNCT_1:def 6;
w = [:h,f:].p by A25,A23,A13,A27,A29,FUNCT_1:def 4;
hence thesis by A28,A4,SS,A12,ZFMISC_1:87;
end;
then p in Fr NM by A21,A4,Th3,A15;
then p in [#]NM\Int NM by SUBSET_1:def 4;
hence thesis by XBOOLE_0:def 5,A1;
end;
suppose
not y in IM;
then y in [#]M\IM by XBOOLE_0:def 5;
then y in Fr M by SUBSET_1:def 4;
then consider W be a_neighborhood of y,m be Nat, f be Function of
M|W,Tdisk(0.TOP-REAL m,1) such that
A30: f is being_homeomorphism
and
A31: f.y in Sphere(0.TOP-REAL m,1) by Th3;
A32: y in Int W by CONNSP_2:def 1;
consider U be a_neighborhood of x,n be Nat such that
A33: N|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def1;
reconsider mn = n+m as Nat;
set TRm=TOP-REAL m,TRn=TOP-REAL n,TRnm=TOP-REAL mn;
consider h be Function of N|U,Tdisk(0.TRn,1) such that
A34: h is being_homeomorphism by A33,T_0TOPSP:def 1;
A35: not f.y in Ball(0.TRm,1) by TOPREAL9:19,A31,XBOOLE_0:3;
consider hf be Function of [: Tdisk(0.TRn,1),Tdisk( 0.TRm,1):],
Tdisk(0.TRnm,1) such that
A36: hf is being_homeomorphism
and
A37: hf.:[:Ball(0.TRn,1), Ball(0.TRm,1):] = Ball(0.TRnm,1) by TIETZE_2:19;
set H=hf*[:h,f:];
[:h,f:] is being_homeomorphism by A30,A34,TIETZE_2:15;
then
A38: H is being_homeomorphism by A36,TOPS_2:57;
then
A39: rng H = [#]Tdisk(0.TRnm,1) by TOPS_2:def 5;
A40: Int W c= W by TOPS_1:16;
A41: Int U c= U by TOPS_1:16;
x in Int U by CONNSP_2:def 1;
then
A42: [x,y] in [:U,W:] by A41,A40,A32,ZFMISC_1:87;
n+m in NAT by ORDINAL1:def 12;
then
A43: [#]Tdisk(0.TRnm,1) = cl_Ball(0.TRnm,1) by BROUWER:3;
A44: [:N|U,M|W:] = NM| [:U,W:] by BORSUK_3:22;
then dom H = [#](NM| [:U,W:]) by A38,TOPS_2:def 5;
then
A45: p in dom H by A42,A4,PRE_TOPC:def 5;
then
A46: [:h,f:].p in dom hf by FUNCT_1:11;
dom [:h,f:] = [:dom h,dom f:] by FUNCT_3:def 8;
then
DD: [:h,f:].(x,y) = [h.x,f.y] by A45,FUNCT_1:11,A4,FUNCT_3:65;
A48: H.p = hf.([:h,f:].p) by A45,FUNCT_1:12;
H.p in Sphere(0.TRnm,1)
proof
H.p in cl_Ball(0.TRnm,1) by A39,A43,A45,FUNCT_1:def 3;
then
A49: H.p in Sphere(0.TRnm,1)\/Ball(0.TRnm,1) by TOPREAL9:18;
assume not H.p in Sphere(0.TRnm,1);
then H.p in hf.:[:Ball(0.TRn,1), Ball(0.TRm,1):]
by A49,XBOOLE_0:def 3,A37;
then consider w be object such that
A50: w in dom hf
and
A51: w in [:Ball(0.TRn,1), Ball(0.TRm,1):]
and
A52: hf.w =H.p by FUNCT_1:def 6;
w = [:h,f:].p by A48,A46,A36,A50,A52,FUNCT_1:def 4;
hence thesis by A51,A4,DD,A35,ZFMISC_1:87;
end;
then p in Fr NM by A44,A4,Th3,A38;
then p in [#]NM\Int NM by SUBSET_1:def 4;
hence thesis by XBOOLE_0:def 5,A1;
end;
end;
let z be object;
assume
A53: z in [:IN,IM:];
then consider x,y be object such that
A54: x in IN
and
A55: y in IM
and
A56: z=[x,y] by ZFMISC_1:def 2;
reconsider x as Point of N by A54;
consider U be a_neighborhood of x, n such that
A57:N|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A54,Def3;
reconsider y as Point of M by A55;
consider W be a_neighborhood of y, m such that
A58:M|W,Tball(0.TOP-REAL m,1) are_homeomorphic by A55,Def3;
reconsider p=z as Point of NM by A53;
set TRn=TOP-REAL n,TRm=TOP-REAL m;
A59: Tball(0.TRm,1) = TRm|Ball(0.TRm,1) by MFOLD_1:def 2;
reconsider mn=m+n as Nat;
A60:(TOP-REAL mn) | Ball(0.TOP-REAL mn,1) = Tball(0.TOP-REAL mn,1)
by MFOLD_1:def 2;
Tball(0.TRn,1) = TRn|Ball(0.TRn,1) by MFOLD_1:def 2;
then [:N|U,M|W:], (TOP-REAL mn) | Ball(0.TOP-REAL mn,1)
are_homeomorphic by A59,A57,A58,TIETZE_2:20;
then NM| [:U,W:],Tball(0.TOP-REAL mn,1) are_homeomorphic
by BORSUK_3:22,A60;
hence thesis by Def3, A56;
end;
theorem Th7:
for N,M be locally_euclidean non empty TopSpace holds
Fr [:N,M:] = [:[#]N,Fr M:] \/ [:Fr N,[#]M:]
proof
let N,M be locally_euclidean non empty TopSpace;
thus Fr [:N,M:] = ([#] [:N,M:]) \Int [:N,M:] by SUBSET_1:def 4
.= ([:[#]N,[#]M:]) \Int [:N,M:] by BORSUK_1:def 2
.= ([:[#]N,[#]M:])\ [:Int N,Int M:] by Th6
.= [:([#]N)\Int N,[#]M:]\/ ([:[#]N,([#]M)\Int M:])
by ZFMISC_1:103
.= [:([#]N)\Int N,[#]M:]\/ ([:[#]N,Fr M:]) by SUBSET_1:def 4
.= [:[#]N,Fr M:]\/[:Fr N,[#]M:] by SUBSET_1:def 4;
end;
registration
let N,M be without_boundary locally_euclidean non empty TopSpace;
cluster [:N,M:] -> without_boundary;
coherence
proof
Int [:N,M:] = [:Int N,Int M:] by Th6
.= [:the carrier of N,Int M:] by Def5
.= [:the carrier of N,the carrier of M:] by Def5
.= the carrier of [:N,M:] by BORSUK_1:def 2;
hence thesis;
end;
end;
registration
let N be locally_euclidean non empty TopSpace;
let M be with_boundary locally_euclidean non empty TopSpace;
cluster [:N,M:] -> with_boundary;
coherence
proof
Fr [:N,M:] = [: [#]N,Fr M:] \/ [: Fr N,[#]M:] by Th7;
hence thesis;
end;
cluster [:M,N:] -> with_boundary;
coherence
proof
Fr [:M,N:] = [: [#]M,Fr N:] \/ [: Fr M,[#]N:] by Th7;
hence thesis;
end;
end;
begin :: Fixed Dimension Locally Euclidean Spaces
definition
let n;
let M be n-locally_euclidean non empty TopSpace;
redefine func Int M -> Subset of M means :Def6:
for p be Point of M holds
p in it
iff
ex U being a_neighborhood of p st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
compatibility
proof
let I be Subset of M;
thus I=Int M implies for p be Point of M holds p in I iff ex U being
a_neighborhood of p st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
assume
A1: I = Int M;
let p be Point of M;
thus p in I implies ex U being a_neighborhood of p st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
consider W be a_neighborhood of p such that
A2: M|W,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
A3: p in Int W by CONNSP_2:def 1;
assume p in I;
then consider U be a_neighborhood of p, m such that
A4: M|U,Tball(0.TOP-REAL m,1) are_homeomorphic by A1,Def3;
A: Tball(0.TOP-REAL m,1) = (TOP-REAL m) |Ball(0.TOP-REAL m,1)
by MFOLD_1:def 2;
p in Int U by CONNSP_2:def 1;
then n=m by A,A3,XBOOLE_0:3,A4,A2,BROUWER3:15;
hence thesis by A4;
end;
thus thesis by Def3,A1;
end;
assume
A5: for p be Point of M holds p in I iff ex U being a_neighborhood of p
st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
thus I c= Int M
proof
let x be object;
assume
A6: x in I;
then reconsider x as Point of M;
ex U being a_neighborhood of x st M|U,Tball(0.TOP-REAL n,1)
are_homeomorphic by A6,A5;
hence thesis by Def3;
end;
let x be object;
assume
A7: x in Int M;
then reconsider x as Point of M;
consider U be a_neighborhood of x, m such that
A8: M|U,Tball(0.TOP-REAL m,1) are_homeomorphic by A7,Def3;
A: Tball(0.TOP-REAL m,1) = (TOP-REAL m) |Ball(0.TOP-REAL m,1)
by MFOLD_1:def 2;
consider W be a_neighborhood of x such that
A9: M|W,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
A10: x in Int W by CONNSP_2:def 1;
x in Int U by CONNSP_2:def 1;
then m=n by A,A10,XBOOLE_0:3,BROUWER3:15,A8,A9;
hence thesis by A5,A8;
end;
coherence;
end;
definition
let n;
let M be n-locally_euclidean non empty TopSpace;
redefine func Fr M -> Subset of M means
for p be Point of M holds
p in it
iff
ex U being a_neighborhood of p,
h be Function of M|U,Tdisk(0.TOP-REAL n,1) st
h is being_homeomorphism & h.p in Sphere(0.TOP-REAL n,1);
compatibility
proof
set TR=TOP-REAL n;
let F be Subset of M;
thus F=Fr M implies for p be Point of M holds p in F iff ex U being
a_neighborhood of p,h be Function of M|U,Tdisk(0.TR,1) st
h is being_homeomorphism & h.p in Sphere(0.TR,1)
proof
assume
A1: F = Fr M;
let p be Point of M;
thus p in F implies ex U being a_neighborhood of p,h be Function of M|U,
Tdisk(0.TR,1) st h is being_homeomorphism & h.p in Sphere(0.TR,1)
proof
consider W be a_neighborhood of p such that
A2: M|W,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
A3: p in Int W by CONNSP_2:def 1;
assume p in F;
then consider U be a_neighborhood of p,m be Nat, h be Function of M|U,
Tdisk(0.TOP-REAL m,1) such that
A4: h is being_homeomorphism
and
A5: h.p in Sphere(0.TOP-REAL m,1) by A1,Th3;
A6: p in Int U by CONNSP_2:def 1;
M|U,Tdisk(0.TOP-REAL m,1) are_homeomorphic by A4,T_0TOPSP:def 1;
then n=m by A3,A6,XBOOLE_0:3,A2,BROUWER3:14;
hence thesis by A4,A5;
end;
thus thesis by Th3,A1;
end;
assume
A7:for p be Point of M holds p in F iff ex U being a_neighborhood of p,
h be Function of M|U,Tdisk(0.TR,1) st h is being_homeomorphism &
h.p in Sphere(0.TR,1);
thus F c= Fr M
proof
let x be object;
assume
A8: x in F;
then reconsider x as Point of M;
ex U being a_neighborhood of x,h be Function of M|U,Tdisk(0.TR,1)
st h is being_homeomorphism & h.x in Sphere(0.TR,1) by A8,A7;
hence thesis by Th3;
end;
let x be object;
assume
A9: x in Fr M;
then reconsider x as Point of M;
consider U be a_neighborhood of x,m be Nat,
h be Function of M|U, Tdisk(0.TOP-REAL m,1) such that
A10: h is being_homeomorphism
and
A11: h.x in Sphere(0.TOP-REAL m,1) by A9,Th3;
A12: x in Int U by CONNSP_2:def 1;
consider W be a_neighborhood of x such that
A13: M|W,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
A14: x in Int W by CONNSP_2:def 1;
M|U,Tdisk(0.TOP-REAL m,1) are_homeomorphic by A10, T_0TOPSP:def 1;
then n=m by A14,A12,XBOOLE_0:3,A13,BROUWER3:14;
hence thesis by A10,A11,A7;
end;
coherence;
end;
theorem
M1 is locally_euclidean & M1,M2 are_homeomorphic implies
M2 is locally_euclidean
proof
assume that
A1: M1 is locally_euclidean
and
A2: M1,M2 are_homeomorphic;
let p be Point of M2;
consider h be Function of M2,M1 such that
A3: h is being_homeomorphism by A2,T_0TOPSP:def 1;
reconsider hp=h.p as Point of M1;
consider U be a_neighborhood of hp,n such that
A4:M1|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A1;
A5: rng h=[#]M1 by A3,TOPS_2:def 5;
then
A6:h.:(h"U)=U by FUNCT_1:77;
then reconsider hhU=h| (h"U) as Function of M2| (h"U),M1|U
by JORDAN24:12;
A7: h"(Int U) c= h"U by TOPS_1:16,RELAT_1:143;
hhU is being_homeomorphism by A3,A6,METRIZTS:2;
then
A8: M2| (h"U), M1| U are_homeomorphic by T_0TOPSP:def 1;
h"(Int U) is open by A5,A3,TOPS_2:43;
then
A9:h"(Int U) c= Int (h"U) by A7,TOPS_1:24;
A10: dom h = [#]M2 by A3,TOPS_2:def 5;
hp in Int U by CONNSP_2:def 1;
then p in h"(Int U) by FUNCT_1:def 7,A10;
then h"U is a_neighborhood of p by A9,CONNSP_2:def 1;
hence thesis by A8,A4,BORSUK_3:3;
end;
theorem Th9:
M1 is n-locally_euclidean & M2 is locally_euclidean &
M1,M2 are_homeomorphic implies M2 is n-locally_euclidean
proof
assume that
A1: M1 is n-locally_euclidean
and
A2: M2 is locally_euclidean
and
A3: M1,M2 are_homeomorphic;
consider h be Function of M1,M2 such that
A4: h is being_homeomorphism by A3,T_0TOPSP:def 1;
let q be Point of M2;
set hp=q;
consider W be a_neighborhood of hp,m such that
A5:M2|W,Tdisk(0.TOP-REAL m,1) are_homeomorphic by A2;
A6: rng h=[#]M2 by A4,TOPS_2:def 5;
then
A7: h"W is non empty by RELAT_1:139;
A8: dom h = [#]M1 by A4,TOPS_2:def 5;
then consider p be object such that
A9: p in [#]M1
and
A10: h.p=q by A6,FUNCT_1:def 3;
reconsider p as Point of M1 by A9;
consider U be a_neighborhood of p such that
A11:M1|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A1;
consider h2 be Function of M2|W,Tdisk(0.TOP-REAL m,1) such that
A12: h2 is being_homeomorphism by T_0TOPSP:def 1,A5;
A13:h.:(h"W)=W by A6,FUNCT_1:77;
then reconsider hhW=h| (h"W) as Function of M1| (h"W), M2| W
by JORDAN24:12;
hhW is being_homeomorphism by A4, A13,METRIZTS:2;
then h2*hhW is being_homeomorphism by A7,A12,TOPS_2:57;
then
A14:M1| (h"W),Tdisk(0.TOP-REAL m,1) are_homeomorphic by T_0TOPSP:def 1;
A15: h"(Int W) c= h"W by TOPS_1:16,RELAT_1:143;
h"(Int W) is open by A6, A4,TOPS_2:43;
then
A16:h"(Int W) c= Int (h"W) by A15,TOPS_1:24;
hp in Int W by CONNSP_2:def 1;
then
A17:p in h"(Int W) by A10,FUNCT_1:def 7,A8;
p in Int U by CONNSP_2:def 1;
then n=m by A17,A16,XBOOLE_0:3,A14,A11,BROUWER3:14;
hence thesis by A5;
end;
::$N Topological Invariance of Dimension of Locally Euclidean Spaces
theorem
M is n-locally_euclidean & M is m-locally_euclidean implies n = m
proof
assume that
A1: M is n-locally_euclidean
and
A2: M is m-locally_euclidean;
set p = the Point of M;
consider W be a_neighborhood of p such that
A3:M|W,Tdisk(0.TOP-REAL m,1) are_homeomorphic by A2;
consider U be a_neighborhood of p such that
A4:M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A1;
A5: p in Int W by CONNSP_2:def 1;
p in Int U by CONNSP_2:def 1;
hence thesis by A5,XBOOLE_0:3,A4,A3,BROUWER3:14;
end;
theorem Th11:
M is without_boundary n-locally_euclidean non empty TopSpace
iff
for p be Point of M ex U be a_neighborhood of p st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
set TR=TOP-REAL n;
hereby
assume
A1: M is without_boundary n-locally_euclidean non empty TopSpace;
then reconsider MM=M as without_boundary n-locally_euclidean
non empty TopSpace;
let p be Point of M;
consider U be a_neighborhood of p such that
A2: M|U,Tdisk(0.TR,1) are_homeomorphic by Def2,A1;
set MU=M|U;
consider h be Function of MU,Tdisk(0.TR,1) such that
A3: h is being_homeomorphism by A2,T_0TOPSP:def 1;
A4: [#]Tdisk(0.TR,1) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider B=Ball(0.TR,1) as Subset of Tdisk(0.TR,1)
by TOPREAL9:16;
reconsider B as open Subset of Tdisk(0.TR,1) by TSEP_1:9;
A5: Int U c= U by TOPS_1:16;
set HIB = B /\ h.:(Int U);
reconsider hib=HIB as Subset of TR by A4,XBOOLE_1:1;
A6: HIB c= Ball(0.TR,1) by XBOOLE_1:17;
A7: h"HIB c= h"(h.:Int U) by XBOOLE_1:17,RELAT_1:143;
AA: h"(h.:Int U) c= Int U by A3,FUNCT_1:82;
A9: cl_Ball(0.TR,1) = Ball(0.TR,1) \/ Sphere(0.TR,1) by TOPREAL9:18;
A10:[#]MU = U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
A11:p in Int U by CONNSP_2:def 1;
A12: dom h = [#]MU by A3,TOPS_2:def 5;
then
A13: h.p in rng h by A11,A5,A10,FUNCT_1:def 3;
A14: h.p in Ball(0.TR,1)
proof
assume not h.p in Ball(0.TR,1);
then h.p in Sphere(0.TR,1) by A4,A13,A9,XBOOLE_0:def 3;
then p in Fr MM by A3,Th3;
hence contradiction;
end;
IU is open by TSEP_1:9;
then h.:(Int U) is open by A3,TOPGRP_1:25;
then
A15: hib is open by TSEP_1:9,A6;
h.p in h.:(Int U) by A11,A5,A10,A12,FUNCT_1:def 6;
then h.p in hib by A14,XBOOLE_0:def 4;
then consider BB be ball Subset of TOP-REAL n such that
A16: BB c= hib
and
A17: h.p in BB by A15,MFOLD_1:3;
reconsider bb=BB as non empty Subset of Tdisk(0.TR,1)
by A16,A17,XBOOLE_1:1;
reconsider hb=h"bb as Subset of M by A10,XBOOLE_1:1;
bb is open by TSEP_1:9;
then
A18:h"bb is open by A3,TOPGRP_1:26;
A19:M|hb = M|U | (h"bb) by A10,PRE_TOPC:7;
hb c= h"HIB by A16,RELAT_1:143;
then hb c= Int U by A7,AA;
then
A20:hb is open by A10,TSEP_1:9,A18,A5;
p in hb by A17, A11,A5,A10,A12,FUNCT_1:def 7;
then
A21: p in Int hb by A20,TOPS_1:23;
consider q be Point of TOP-REAL n, r be Real such that
A22: BB = Ball(q,r) by MFOLD_1:def 1;
rng h = [#]Tdisk(0.TR,1) by A3,TOPS_2:def 5;
then
A23: h.: (h"bb) = bb by FUNCT_1:77;
A24:TR|Ball(q,r) = Tball(q,r) by MFOLD_1:def 2;
A25: Tdisk(0.TR,1) | bb = TR|Ball(q,r) by A4,A22,PRE_TOPC:7;
then reconsider hh=h| (h"bb) as Function of M|hb,Tball(q,r)
by A19,JORDAN24:12,A23,A24;
reconsider hb as a_neighborhood of p by A21,CONNSP_2:def 1;
hh is being_homeomorphism by A3,A19,A23,A24,A25,METRIZTS:2;
then
A26: M|hb,Tball(q,r) are_homeomorphic by T_0TOPSP:def 1;
take hb;
A27:r>0 by A17,A22;
then Tball(q,r),Tball(0.TR,1) are_homeomorphic by MFOLD_1:9;
hence M|hb,Tball(0.TR,1) are_homeomorphic by A26,BORSUK_3:3,A27;
end;
assume
A28:for p be Point of M ex U being a_neighborhood of p st
M|U,Tball(0.TR,1) are_homeomorphic;
M is n-locally_euclidean
proof
[#]Tdisk(0.TR,1) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider B=Ball(0.TR,1) as Subset of Tdisk(0.TR,1)
by TOPREAL9:16;
reconsider B as open Subset of Tdisk(0.TR,1) by TSEP_1:9;
let p be Point of M;
consider U be a_neighborhood of p such that
A29: M|U,Tball(0.TR,1) are_homeomorphic by A28;
N: n in NAT by ORDINAL1:def 12;
A30:Tball(0.TR,1) = TR|Ball(0.TR,1) by MFOLD_1:def 2;
then
A31: [#]Tball(0.TR,1) = Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider clB = cl_Ball(0.TR,1/2) as non empty Subset of
Tball(0.TR,1) by JORDAN:21,N;
set MU=M|U;
consider h be Function of MU,Tball(0.TR,1) such that
A32: h is being_homeomorphism by A29,T_0TOPSP:def 1;
set En=Euclid n;
A33: Int U c= U by TOPS_1:16;
A34: [#]MU = U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
reconsider hIU = h.:IU as Subset of TR by A31,XBOOLE_1:1;
A36: dom h = [#]MU by A32,TOPS_2:def 5;
then
A37: IU=h"hIU by A32,FUNCT_1:82,FUNCT_1:76;
A38:the TopStruct of TR = TopSpaceMetr En by EUCLID:def 8;
then reconsider hIUE=hIU as Subset of TopSpaceMetr En;
A39:p in Int U by CONNSP_2:def 1;
then
A40: h.p in hIU by A36,FUNCT_1:def 6;
then reconsider hp=h.p as Point of En by EUCLID:67;
reconsider Hp=h.p as Point of TR by A40;
IU is open by TSEP_1:9;
then h.:IU is open by A32,TOPGRP_1:25;
then hIU is open by A31,TSEP_1:9;
then hIU in the topology of TR by PRE_TOPC:def 2;
then consider r be Real such that
A41: r > 0
and
A42: Ball(hp,r) c= hIUE by A40,A38,PRE_TOPC:def 2,TOPMETR:15;
set r2=r/2;
A43: Ball(Hp,r)=Ball(hp,r) by TOPREAL9:13;
cl_Ball(Hp,r2) c= Ball(Hp,r) by N,XREAL_1:216,A41,JORDAN:21;
then
A44: cl_Ball(Hp,r2) c= hIU by A42,A43;
then
reconsider CL=cl_Ball(Hp,r2) as Subset of Tball(0.TR,1) by XBOOLE_1:1;
A45: cl_Ball(Hp,r2) c= [#]Tball(0.TR,1) by A44,XBOOLE_1:1;
then cl_Ball(Hp,r2) c= rng h by A32,TOPS_2:def 5;
then
A46: h.:(h"CL) = CL by FUNCT_1:77;
set r22=r2/2;
r22 < r2 by A41,XREAL_1:216;
then
A47: Ball(Hp,r22) c= Ball(Hp,r2) by N,JORDAN:18;
reconsider hCL=h"CL as Subset of M by A34,XBOOLE_1:1;
A48: (M|U) | (h"CL) = M| hCL by A34,PRE_TOPC:7;
A49: Ball(Hp,r2) c= cl_Ball(Hp,r2) by TOPREAL9:16;
then
A50:Ball(Hp,r22) c= cl_Ball(Hp,r2) by A47;
then reconsider BI = Ball(Hp,r22) as Subset of Tball(0.TR,1)
by A45,XBOOLE_1:1;
BI c= hIU by A44,A49,A47;
then
A51: h"BI c= h"hIU by RELAT_1:143;
reconsider hBI=h"BI as Subset of M by A34,XBOOLE_1:1;
BI is open by TSEP_1:9;
then h"BI is open by A32,TOPGRP_1:26;
then
A52: hBI is open by A37,A51,TSEP_1:9;
|.Hp - Hp.|=0 by TOPRNS_1:28;
then h.p in BI by A41;
then p in h"BI by A39,A33,A34,A36,FUNCT_1:def 7;
then p in Int hCL by A50,RELAT_1:143,TOPS_1:22,A52;
then reconsider hCL as a_neighborhood of p by CONNSP_2:def 1;
A53: Tball(0.TR,1) |CL = Tdisk(Hp,r2) by A30,A31,PRE_TOPC:7;
then reconsider hh=h| (h"CL) as Function of M|hCL ,Tdisk(Hp,r2)
by A46,JORDAN24:12,A48;
hh is being_homeomorphism by A32,A53,METRIZTS:2,A46,A48;
then
A54:M|hCL,Tdisk(Hp,r2) are_homeomorphic by T_0TOPSP:def 1;
Tdisk(Hp,r2),Tdisk(0.TR,1) are_homeomorphic by Lm1,A41;
hence thesis by A54,BORSUK_3:3,A41;
end;
then reconsider M as n-locally_euclidean non empty TopSpace;
M is without_boundary
proof
thus Int M c= the carrier of M;
let x be object;
assume x in the carrier of M;
then reconsider p=x as Point of M;
ex U being a_neighborhood of p st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A28;
hence thesis by Def3;
end;
hence thesis;
end;
registration
let n,m be Element of NAT;
let N be n-locally_euclidean non empty TopSpace;
let M be m-locally_euclidean non empty TopSpace;
::$N Dimension of the Cartesian Product of Locally Euclidean Spaces
cluster [:N,M:] -> (n+m)-locally_euclidean;
coherence
proof
reconsider nm=n+m as Nat;
let p be Point of [:N,M:];
ex hf be Function of
[: Tdisk( 0.TOP-REAL n,1),Tdisk( 0.TOP-REAL m,1):],
Tdisk(0.TOP-REAL (n+m),1) st
hf is being_homeomorphism &
hf.:[:Ball( 0.TOP-REAL n,1), Ball(0.TOP-REAL m,1):] =
Ball(0. TOP-REAL nm,1) by TIETZE_2:19;
then
A1: [: Tdisk( 0.TOP-REAL n,1),Tdisk( 0.TOP-REAL m,1):],
Tdisk(0.TOP-REAL nm,1) are_homeomorphic by T_0TOPSP:def 1;
p in the carrier of [:N,M:];
then p in [:the carrier of N,the carrier of M:] by BORSUK_1:def 2;
then consider x,y be object such that
A2: x in the carrier of N
and
A3: y in the carrier of M
and
A4: p=[x,y] by ZFMISC_1: def 2;
reconsider x as Point of N by A2;
consider Ux be a_neighborhood of x such that
A5: N|Ux,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
reconsider y as Point of M by A3;
consider Uy be a_neighborhood of y such that
A6: M|Uy,Tdisk(0.TOP-REAL m,1) are_homeomorphic by Def2;
consider hy be Function of M|Uy,Tdisk(0.TOP-REAL m,1) such that
A7: hy is being_homeomorphism by A6,T_0TOPSP:def 1;
consider hx be Function of N|Ux,Tdisk(0.TOP-REAL n,1) such that
A8: hx is being_homeomorphism by A5,T_0TOPSP:def 1;
[:hx,hy:] is being_homeomorphism by A7,TIETZE_2:15,A8;
then
A9: [:N|Ux,M|Uy:],[:Tdisk(0.TOP-REAL n,1),Tdisk(0.TOP-REAL m,1):]
are_homeomorphic by T_0TOPSP:def 1;
[:N|Ux,M|Uy:] = [:N,M:] | [:Ux,Uy:] by BORSUK_3:22;
hence thesis by A1,A9,BORSUK_3:3,A4;
end;
end;
registration
let n;
let M be n-locally_euclidean non empty TopSpace;
::$N Dimension of the Interior of Locally Euclidean Spaces
cluster M|Int M -> n-locally_euclidean for non empty TopSpace;
coherence
proof
set MI=M|Int M;
A1: [#]MI=Int M by PRE_TOPC:def 5;
for p be Point of MI ex U being a_neighborhood of p st
MI|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
let p be Point of MI;
p in Int M by A1;
then reconsider q=p as Point of M;
consider U be a_neighborhood of q such that
A2: M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A1,Def6;
set MU=M|U,TR=TOP-REAL n;
consider h be Function of MU,Tball(0.TR,1) such that
A3: h is being_homeomorphism by A2,T_0TOPSP:def 1;
A4: Int U c= U by TOPS_1:16;
A5: Int M /\ Int U in the topology of M by PRE_TOPC:def 2;
A6: Int U c= U by TOPS_1:16;
A7: [#]MU = U by PRE_TOPC:def 5;
Int U /\ Int M c= Int U by XBOOLE_1:17;
then reconsider UIM = Int M /\ Int U as Subset of MU
by A6,A7,XBOOLE_1:1;
A8: h"(h.:UIM) c= UIM by A3,FUNCT_1:82;
A9: dom h =[#]MU by A3,TOPS_2:def 5;
A11: Tball(0.TR,1) = TR|Ball(0.TR,1) by MFOLD_1:def 2;
then
A12: [#]Tball(0.TR,1) = Ball(0.TR,1) by PRE_TOPC:def 5;
then reconsider hum=h.:UIM as Subset of TR by XBOOLE_1:1;
UIM /\[#]MU = UIM by XBOOLE_1:28;
then UIM in the topology of MU by A5,PRE_TOPC:def 4;
then UIM is open by PRE_TOPC:def 2;
then h.:UIM is open by A3,TOPGRP_1:25;
then hum is open by TSEP_1:9,A12;
then
A13: Int hum = hum by TOPS_1:23;
A14: q in Int U by CONNSP_2:def 1;
then
A15: q in UIM by A1,XBOOLE_0:def 4;
then h.q in hum by A9,FUNCT_1:def 6;
then reconsider hq=h.q as Point of TR;
reconsider HQ=hq as Point of Euclid n by EUCLID:67;
h.q in h.:UIM by A15,A9,FUNCT_1:def 6;
then consider s be Real such that
A16: s>0 and
A17: Ball(HQ,s) c= hum by A13,GOBOARD6:5;
A18: Ball(HQ,s)=Ball(hq,s) by TOPREAL9:13;
then reconsider BB=Ball(hq,s) as Subset of Tball(0.TR,1)
by A17,XBOOLE_1:1;
BB is open by TSEP_1:9;
then reconsider hBB=h"BB as open Subset of MU by A3,TOPGRP_1:26;
hBB c= h"(h.:UIM) by A17,A18,RELAT_1:143;
then
A19: hBB c= UIM by A8;
reconsider hBBM=hBB as Subset of M by A7,XBOOLE_1:1;
Int U /\ Int M c= Int M by XBOOLE_1:17;
then reconsider HBB=hBBM as Subset of MI by A19,XBOOLE_1:1,A1;
hBBM is open by TSEP_1:9,A19;
then
A20: HBB is open by TSEP_1:9;
|.hq-hq.|=0 by TOPRNS_1:28;
then hq in BB by A16;
then p in HBB by FUNCT_1:def 7,A14,A4,A9,A7;
then
A21: p in Int HBB by A20,TOPS_1:23;
A22: M|hBBM = MI|HBB by A1,PRE_TOPC:7;
rng h = [#]Tball(0.TR,1) by A3,TOPS_2:def 5;
then h.:hBB=BB by FUNCT_1:77;
then
A23: Tball(0.TR,1) | (h.:hBB) = TR|Ball(hq,s) by A11,A12,PRE_TOPC:7;
reconsider HBB as a_neighborhood of p by A21,CONNSP_2:def 1;
A24: MU|hBB =M|hBBM by A7,PRE_TOPC:7;
then reconsider hh=h|hBB as Function of MI|HBB,TR|Ball(hq,s)
by A23,JORDAN24:12,A22;
hh is being_homeomorphism by A3,A23,A24,A22,METRIZTS:2;
then MI|HBB,TR|Ball(hq,s) are_homeomorphic by T_0TOPSP:def 1;
then
A25: MI|HBB,Tball(hq,s) are_homeomorphic by MFOLD_1:def 2;
take HBB;
Tball(hq,s),Tball(0.TR,1) are_homeomorphic by A16,MFOLD_1:9;
hence thesis by A16,A25,BORSUK_3:3;
end;
hence thesis by Th11;
end;
end;
registration
let n be non zero Nat;
let M be with_boundary n-locally_euclidean non empty TopSpace;
::$N Dimension of the Boundary of Locally Euclidean Spaces
cluster M|Fr M -> (n-'1)-locally_euclidean for non empty TopSpace;
coherence
proof
set MF=M|Fr M;
n >0;
then reconsider n1=n-1 as Nat by NAT_1:20;
A1: [#]MF=Fr M by PRE_TOPC:def 5;
A2: now
let pF be Point of MF;
pF in [#]MF;
then reconsider p=pF as Point of M by A1;
consider U be a_neighborhood of p such that
A3: M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
M|U,Tdisk(0.TOP-REAL (n1+1),1) are_homeomorphic by A3;
hence ex W being a_neighborhood of pF st
MF |W,Tball(0.TOP-REAL n1,1) are_homeomorphic by Th5;
end;
n-'1 = n1 by XREAL_0:def 2;
hence thesis by A2,Th11;
end;
end;
begin :: Connected Components of Locally Euclidean Spaces
theorem Th12:
for M be compact locally_euclidean non empty TopSpace
for C be Subset of M st C is a_component holds
C is open &
ex n st M|C is n-locally_euclidean non empty TopSpace
proof
let M be compact locally_euclidean non empty TopSpace;
defpred P[Point of M,Subset of M] means $2 is a_neighborhood of $1 & ex n st
M|$2,Tdisk(0.TOP-REAL n,1) are_homeomorphic;
let C be Subset of M such that
A1: C is a_component;
consider p be object such that
A2:p in C by A1,XBOOLE_0:def 1;
reconsider p as Point of M by A2;
A3:for x be Point of M ex y be Element of bool the carrier of M st P[x,y]
proof
let x be Point of M;
ex U be a_neighborhood of x,n st M|U,Tdisk(0.TOP-REAL n,1)
are_homeomorphic by Def1;
hence thesis;
end;
consider W be Function of M,bool the carrier of M such that
A4: for x be Point of M holds P[x,W.x] from FUNCT_2:sch 3(A3);
reconsider MC =M|C as non empty connected TopSpace by A1,CONNSP_1:def 3;
defpred CC[object,object] means $2 in C & for A be Subset of M st A=W.$2
holds Int A= $1;
set IntW = {Int U where U is Subset of M:U in rng (W|C)};
IntW c= bool the carrier of M
proof
let x be object;
assume x in IntW;
then ex U be Subset of M st x = Int U & U in rng (W|C);
hence thesis;
end;
then reconsider IntW as Subset-Family of M;
reconsider R=IntW\/{C`} as Subset-Family of M;
for A be Subset of M st A in R holds A is open
proof
let A be Subset of M such that
A5: A in R;
per cases by ZFMISC_1:136,A5;
suppose
A=C`;
hence thesis by A1;
end;
suppose
A in IntW;
then ex U be Subset of M st A=Int U & U in rng (W|C);
hence thesis;
end;
end;
then
A6: R is open by TOPS_2:def 1;
A7: for A be Subset of M st A in rng W holds
A is connected & Int A is non empty
proof
let A be Subset of M;
assume A in rng W;
then consider p be object such that
A8: p in dom W
and
A9: W.p = A by FUNCT_1:def 3;
consider n such that
A10: M|A,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A8,A9,A4;
reconsider AA=A as non empty Subset of M by A8,A9,A4;
A11:Tdisk(0.TOP-REAL n,1) is connected by CONNSP_1:def 3;
Tdisk(0.TOP-REAL n,1), M|AA are_homeomorphic by A10;
then consider h be Function of Tdisk(0.TOP-REAL n,1),M|A such that
A12: h is being_homeomorphism by T_0TOPSP:def 1;
reconsider p as Point of M by A8;
A13: P[p,A] by A8,A9,A4;
A14: rng h = [#](M|A) by A12,TOPS_2:def 5;
A15: h.:dom h = rng h by RELAT_1:113;
dom h = [#]Tdisk(0.TOP-REAL n,1) by A12,TOPS_2:def 5;
then M|A is connected by A15,A14,A12,A11,CONNSP_1:14;
hence thesis by CONNSP_1:def 3,A13,CONNSP_2:def 1;
end;
A16: dom W = the carrier of M by FUNCT_2:def 1;
the carrier of M c= union R
proof
let x be object;
assume x in the carrier of M;
then reconsider x as Point of M;
per cases;
suppose
x in C;
then
A17: x in dom (W|C) by RELAT_1:57,A16;
then
A18: (W|C).x = W.x by FUNCT_1:47;
(W|C).x in rng (W|C) by A17,FUNCT_1:def 3;
then Int (W.x) in IntW by A18;
then
A19: Int (W.x) in R by XBOOLE_0:def 3;
W.x is a_neighborhood of x by A4;
then x in Int (W.x) by CONNSP_2:def 1;
hence thesis by A19,TARSKI:def 4;
end;
suppose
not x in C;
then x in [#]M\C by XBOOLE_0:def 5;
then
A20: x in C` by SUBSET_1:def 4;
C` in R by ZFMISC_1:136;
hence thesis by A20,TARSKI:def 4;
end;
end;
then consider R1 be Subset-Family of M such that
A21: R1 c= R
and
A22: R1 is Cover of M
and
A23: R1 is finite by SETFAM_1:def 11,A6,COMPTS_1:def 1;
reconsider R1 as finite Subset-Family of M by A23;
set R2=R1\{C`};
union R1 = the carrier of M by A22,SETFAM_1:45;
then WW: union R1 \ union {C`} = (the carrier of M) \ C` by ZFMISC_1:25
.= C`` by SUBSET_1:def 4
.= C;
then C c= union R2 by TOPS_2:4;
then consider xp be set such that
p in xp
and
A26: xp in R2 by A2,TARSKI:def 4;
A27: C = Component_of C by A1,CONNSP_3:7;
for x be set holds x in C iff ex Q be Subset of M st
Q is open & Q c= C & x in Q
proof
let x be set;
hereby
assume
A28: x in C;
then reconsider p=x as Point of M;
take I=Int (W.p);
A29: Int (W.p) c= W.p by TOPS_1:16;
W.p in rng W by A16,FUNCT_1:def 3;
then
A30: W.p is connected by A7;
A31: W.p is a_neighborhood of p by A4;
then p in Int (W.p) by CONNSP_2:def 1;
then W.p meets C by A29,A28,XBOOLE_0:3;
then W.p c= C by A1,A30,CONNSP_3:16,A27;
hence I is open & I c= C & x in I by A31,CONNSP_2:def 1,A29;
end;
thus thesis;
end;
hence C is open by TOPS_1:25;
A32: R2 c= R1 by XBOOLE_1:36;
A33: rng (W|C) c= rng W by RELAT_1:70;
union R2 c= C
proof
let x be object;
assume x in union R2;
then consider y be set such that
A34: x in y
and
A35: y in R2 by TARSKI:def 4;
y in R1 by A35,ZFMISC_1:56;
then y in IntW or y = C` by A21,ZFMISC_1:136;
then consider U be Subset of M such that
A36: y=Int U
and
A37: U in rng (W|C) by A35,ZFMISC_1:56;
A38: U is connected by A33,A37,A7;
A39: Int U c= U by TOPS_1:16;
consider p be object such that
A41: p in dom (W|C)
and
A42: (W|C).p = U by A37,FUNCT_1:def 3;
A43: W.p = U by A41,A42,FUNCT_1:47;
p in dom W by A41,RELAT_1:57;
then reconsider p as Point of M;
U is a_neighborhood of p by A4,A43;
then p in Int U by CONNSP_2:def 1;
then W.p meets C by A39,A41,A43,XBOOLE_0:3;
then U c= C by A43,A1,A38,CONNSP_3:16,A27;
hence thesis by A39,A34,A36;
end;
then
A44: union R2 = C by WW,TOPS_2:4;
A45:for x be object st x in R2 ex y be object st CC[x,y]
proof
let x be object;
assume
A46: x in R2;
then
A47: x <>C` by ZFMISC_1:56;
x in R1 by A46,ZFMISC_1:56;
then x in IntW by A21,A47,ZFMISC_1:136;
then consider U be Subset of M such that
A48: x=Int U
and
A49: U in rng (W|C);
consider y be object such that
A50: y in dom (W|C)
and
A51: (W|C).y = U by A49,FUNCT_1:def 3;
take y;
thus y in C by A50;
let A be Subset of M;
thus thesis by A50,FUNCT_1:47,A48,A51;
end;
consider cc be Function such that
A52: dom cc = R2 & for x be object st x in R2 holds CC[x,cc.x]
from CLASSES1:sch 1(A45);
CC[xp,cc.xp] by A26,A52;
then reconsider cp = cc.xp as Point of M;
consider n such that
A53: M| (W.cp),Tdisk(0.TOP-REAL n,1) are_homeomorphic by A4;
defpred P[Nat] means $1 <= card R2 implies
ex R3 be Subset-Family of M st
card R3 = $1 &
R3 c= R2 &
union (W.:(cc.:R3)) is connected Subset of M &
for A,B be Subset of M st A in R3 & B=W.(cc.A)
holds M|B,Tdisk(0.TOP-REAL n,1) are_homeomorphic;
A54: Int (W.cp) = xp by A26,A52;
A55: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A56:P[k];
assume
A57: k+1 <= card R2;
then consider R3 be Subset-Family of M such that
A58: card R3 = k
and
A59: R3 c= R2
and
A60: union (W.:(cc.:R3)) is connected Subset of M
and
A61: for A,B be Subset of M st A in R3 & B=W.(cc.A) holds M| B,Tdisk
(0.TOP-REAL n,1) are_homeomorphic by NAT_1:13,A56;
k < card R2 by A57,NAT_1:13;
then k in Segm (card R2) by NAT_1:44;
then R2\R3 <> {} by A58,CARD_1:68;
then consider r23 be object such that
A62: r23 in R2\R3 by XBOOLE_0:def 1;
reconsider r23 as set by TARSKI:1;
A63: r23 in R2 by A62,XBOOLE_0:def 5;
then
A64: r23 <> C` by ZFMISC_1:56;
r23 in R1 by A63,ZFMISC_1:56;
then r23 in IntW by A21,A64,ZFMISC_1:136;
then
A65:ex B be Subset of M st Int B = r23 & B in rng (W|C);
A66: r23 c= union (R2\R3) by A62,ZFMISC_1:74;
per cases;
suppose
k>0;
then R3 is non empty by A58;
then consider r3 be set such that
A67: r3 in R3;
A68: r3 <> C` by A59,A67,ZFMISC_1:56;
r3 in R1 by A59,A67,ZFMISC_1:56;
then r3 in IntW by A21,A68,ZFMISC_1:136;
then
A69: ex A be Subset of M st Int A = r3 & A in rng (W|C);
r3 c= union R3 by A67,ZFMISC_1:74;
then reconsider U3=union R3 as non empty Subset of M
by A33,A69,A7;
set A1 =the Subset of M;
reconsider U23=union (R2\R3) as Subset of M;
set D2=Down(U3,C),D23=Down(U23,C);
D2 = U3/\C by CONNSP_3:def 5;
then
A70: D2 = U3 by XBOOLE_1:28, A44,A59,ZFMISC_1:77;
(R2\R3) \/R3 = R2\/R3 by XBOOLE_1:39
.= R2 by A59,XBOOLE_1:12;
then U3\/U23 = C by A44,ZFMISC_1:78;
then
A71: U3\/U23 =[#]MC by PRE_TOPC:def 5;
R3 c= R1 by A32,A59;
then R3 is open by A21,XBOOLE_1:1,A6,TOPS_2:11;
then
A72: D2 is open by TOPS_2:19,CONNSP_3:28;
A73: R2\R3 c= R2 by XBOOLE_1:36;
then R2\R3 c= R1 by A32;
then R2\R3 is open by A21,XBOOLE_1:1,A6,TOPS_2:11;
then
A74: D23 is open by TOPS_2:19,CONNSP_3:28;
D23 = U23 /\C by CONNSP_3:def 5;
then
A75: D23 =U23 by XBOOLE_1:28,A73,A44,ZFMISC_1:77;
U23<>{}MC by A66,A33,A65,A7;
then consider m be object such that
A76: m in U3
and
A77: m in U23 by A72,A74,A70,A75,A71,CONNSP_1:11,XBOOLE_0:3;
consider m1 be set such that
A78: m in m1
and
A79: m1 in R3 by A76,TARSKI:def 4;
CC[m1,cc.m1] by A59,A79,A52;
then reconsider c1=cc.m1 as Point of M;
consider m2 be set such that
A80: m in m2
and
A81: m2 in R2\R3 by A77,TARSKI:def 4;
A82: m2 in R2 by A81,XBOOLE_0:def 5;
then CC[m2,cc.m2] by A52;
then reconsider c2=cc.m2 as Point of M;
set R4 = R3\/{Int (W.c2)};
R3 is finite by A58;
then reconsider R4 as finite Subset-Family of M;
take R4;
A83: Int (W.c2) = m2 by A82,A52;
then not Int (W.c2) in R3 by A81,XBOOLE_0:def 5;
hence card R4 = k+1 by A58,A59,CARD_2:41;
A84: m2 in R2 by A81,XBOOLE_0:def 5;
then {m2} c= R2 by ZFMISC_1:31;
hence
A85: R4 c= R2 by A83,A59,XBOOLE_1:8;
A86: W.c2 in rng W by A16,FUNCT_1:def 3;
A87: Int (W.c1) = m1 by A59,A79,A52;
thus union (W.:(cc.:R4)) is connected Subset of M
proof
reconsider UWR3=union (W.:(cc.:R3)) as connected Subset of M by A60;
A88: Int (W.c2) c= W.c2 by TOPS_1:16;
c1 in cc.:R3 by A79, A59,A52,FUNCT_1:def 6;
then
A89: W.c1 in W.:(cc.:R3) by A16,FUNCT_1:def 6;
Int (W.c1) c= W.c1 by TOPS_1:16;
then
A90: m in UWR3 by A89,A87,A78,TARSKI:def 4;
UWR3 c= Cl UWR3 by PRE_TOPC:18;
then Cl UWR3 meets W.c2 by A88,A83,A80, A90,XBOOLE_0:3;
then
A91: not UWR3, (W.c2) are_separated by CONNSP_1:def 1;
cc.:R4 = (cc.:R3) \/ cc.:{m2} by A83,RELAT_1:120
.= (cc.:R3) \/ Im(cc,m2) by RELAT_1:def 16
.= (cc.:R3) \/ {cc.m2} by FUNCT_1:59,A84,A52;
then W.:(cc.:R4) = (W.:(cc.:R3)) \/ W.:{c2} by RELAT_1:120
.= (W.:(cc.:R3)) \/ Im(W,c2) by RELAT_1:def 16
.= (W.:(cc.:R3)) \/ {W.c2} by A16,FUNCT_1:59;
then
A92: union (W.:(cc.:R4)) = UWR3 \/ union {W.c2} by ZFMISC_1:78
.= UWR3 \/ (W.c2) by ZFMISC_1:25;
W.c2 is connected by A86,A7;
hence thesis by A91,CONNSP_1:17,A92;
end;
let a,b be Subset of M such that
A93: a in R4
and
A94: b=W.(cc.a);
per cases by A93,ZFMISC_1:136;
suppose
a in R3;
hence thesis by A94,A61;
end;
suppose
a = Int (W.c2);
then Int b = Int (W.c2) by A82,A52,A94;
then
A95: m in Int b by A82,A52,A80;
CC[a,cc.a] by A93,A85,A52;
then reconsider ca=cc.a as Point of M;
A96: M| (W.c1),Tdisk(0.TOP-REAL n,1) are_homeomorphic by A79, A61;
P[ca,W.ca] by A4;
then consider mm be Nat such that
A97: M|b,Tdisk(0.TOP-REAL mm,1) are_homeomorphic by A94;
Int (W.c1) = m1 by A59,A79,A52;
then n=mm by A96,A78,A95,XBOOLE_0:3,A97, BROUWER3:14;
hence M| b,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A97;
end;
end;
suppose
A98: k=0;
reconsider R3={Int (W.cp)} as Subset-Family of M;
take R3;
thus card R3 = k+1 by A98,CARD_1:30;
thus
A99: R3 c= R2 by A54,A26,ZFMISC_1:31;
cc.:R3 = Im(cc,xp) by A54,RELAT_1:def 16
.= {cp} by FUNCT_1:59,A26,A52;
then W.:(cc.:R3) = Im(W,cp) by RELAT_1:def 16
.={W.cp} by A16,FUNCT_1:59;
then
A100: union (W.:(cc.:R3)) = W.cp by ZFMISC_1:25;
W.cp in rng W by A16,FUNCT_1:def 3;
hence union (W.:(cc.:R3)) is connected Subset of M by A100,A7;
let a,b be Subset of M such that
A101: a in R3
and
A102: b=W.(cc.a);
CC[a,cc.a] by A101,A99,A52;
then reconsider ca=cc.a as Point of M;
Int (W.cp) = xp by A26,A52;
hence M| b,Tdisk(0.TOP-REAL n,1) are_homeomorphic
by A53, TARSKI:def 1,A101,A102;
end;
end;
take n;
A105: P[0]
proof
set R3=the empty Subset of bool the carrier of M;
assume 0<= card R2;
take R3;
thus card R3=0 & R3 c= R2;
reconsider UR3=union (W.:(cc.:R3)) as empty Subset of M by ZFMISC_1:2;
UR3 is connected;
hence union (W.:(cc.:R3)) is connected Subset of M;
let A,B be Subset of M;
thus thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A105,A55);
then P[card R2];
then consider R3 be Subset-Family of M such that
A106: card R3 = card R2
and
A107: R3 c= R2
and
A108: for A,B be Subset of M st A in R3 & B=W.(cc.A) holds
M| B,Tdisk(0.TOP-REAL n,1) are_homeomorphic;
A109:R2 = R3 by A106,A107,CARD_2:102;
for p being Point of MC ex U be a_neighborhood of p st
MC|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic
proof
let q be Point of MC;
A110: [#]MC=C by PRE_TOPC:def 5;
then consider y be set such that
A111: q in y
and
A112: y in R2 by A44,TARSKI:def 4;
CC[y,cc.y] by A52,A112;
then reconsider c = cc.y as Point of M;
reconsider Wc=W.c as Subset of M;
A113: Int Wc c= Wc by TOPS_1:16;
set D=Down(Wc,C),DI= Down(Int Wc,C);
Wc in rng W by A16,FUNCT_1:def 3;
then
A114:Wc is connected by A7;
A115:Int Wc = y by A52,A112;
then Wc meets C by A113,A111, A110,XBOOLE_0:3;
then
A116: Wc c= C by A114,A1,CONNSP_3:16,A27;
then W.c/\C = W.c by XBOOLE_1:28;
then
A117: D = W.c by CONNSP_3:def 5;
(Int Wc)/\C = Int Wc by A116,A113,XBOOLE_1:1, XBOOLE_1:28;
then DI = Int Wc by CONNSP_3:def 5;
then q in Int D by CONNSP_3:28,A111,A115,A117,A113,TOPS_1:22;
then
A118: D is a_neighborhood of q by CONNSP_2:def 1;
M| (W.c) =(M|C) |D by A117,A110,PRE_TOPC:7;
hence thesis by A118, A108,A109,A112;
end;
hence thesis by Def2;
end;
theorem
for M be compact locally_euclidean non empty TopSpace
ex P be a_partition of the carrier of M st
for A be Subset of M st A in P holds
A is open a_component &
ex n st M|A is n-locally_euclidean non empty TopSpace
proof
let M be compact locally_euclidean non empty TopSpace;
set P={Component_of p where p is Point of M: not contradiction};
P c= bool the carrier of M
proof
let x be object;
assume x in P;
then ex p be Point of M st x=Component_of p & not contradiction;
hence thesis;
end;
then reconsider P as Subset-Family of M;
A1: the carrier of M c= union P
proof
let x be object;
assume x in the carrier of M;
then reconsider x as Point of M;
A2: Component_of x in P;
x in Component_of x by CONNSP_1:38;
hence thesis by A2,TARSKI:def 4;
end;
for A be Subset of M st A in P holds A<>{} & for B be Subset of M st
B in P holds A = B or A misses B
proof
let A be Subset of M;
assume A in P;
then consider p be Point of M such that
A3: A=Component_of p
and not contradiction;
thus A <>{} by A3;
let B be Subset of M such that
A4: B in P
and
A5: B<>A;
A6:ex q be Point of M st B=Component_of q & not contradiction by A4;
assume A meets B;
then consider x be object such that
A7: x in A
and
A8: x in B by XBOOLE_0:3;
reconsider x as Point of M by A7;
Component_of p = Component_of x by CONNSP_1:42,A7,A3;
hence thesis by CONNSP_1:42,A8,A6,A5,A3;
end;
then reconsider P as a_partition of the carrier of M
by A1,XBOOLE_0:def 10,EQREL_1:def 4;
take P;
let A be Subset of M;
assume A in P;
then ex p be Point of M st A=Component_of p & not contradiction;
then A is a_component by CONNSP_1:40;
hence thesis by Th12;
end;
theorem
for M be compact locally_euclidean non empty TopSpace st
M is connected
ex n st M is n-locally_euclidean
proof
let M be compact locally_euclidean non empty TopSpace;
A1: for A be Subset of M st A is connected & [#]M c= A holds A=[#]M;
assume M is connected;
then [#]M is a_component by A1,CONNSP_1:27,CONNSP_1:def 5;
then consider n such that
A2: M | [#]M is n-locally_euclidean non empty TopSpace by Th12;
M | [#]M,M are_homeomorphic by MFOLD_1:1;
then M is n-locally_euclidean by Th9,A2;
hence thesis;
end;
begin :: Topological Manifold
registration
let n;
cluster second-countable Hausdorff n-locally_euclidean for
non empty TopSpace;
existence
proof
take T= Tdisk(0.TOP-REAL n,1);
thus thesis;
end;
end;
definition
mode topological_manifold is second-countable Hausdorff locally_euclidean
non empty TopSpace;
end;
notation
let n;
let M be topological_manifold;
synonym M is n-dimensional for M is n-locally_euclidean;
end;
registration
let n;
cluster n-dimensional without_boundary for topological_manifold;
existence
proof
Tball(0.TOP-REAL n,1) =(TOP-REAL n) |Ball(0.TOP-REAL n,1) by MFOLD_1:def 2;
then reconsider T=Tball(0.TOP-REAL n,1) as topological_manifold;
T is without_boundary;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster n-dimensional compact with_boundary for topological_manifold;
existence
proof
reconsider T=Tdisk(0.TOP-REAL n,1) as topological_manifold;
T is compact;
hence thesis;
end;
end;
registration
let M be topological_manifold;
cluster -> second-countable Hausdorff for non empty SubSpace of M;
coherence
proof
let S be non empty SubSpace of M;
[#]S c= [#]M by PRE_TOPC:def 4;
then reconsider CS=[#]S as Subset of M;
consider B be Basis of M|CS such that
A1: card B=weight (M|CS) by WAYBEL23:74;
A2: weight (M|CS) c= omega by WAYBEL23:def 6;
A3: the TopStruct of S = S | [#]S by TSEP_1:93;
A4: S| [#]S is SubSpace of M by TSEP_1:7;
[#](S| [#]S) =[#]S by PRE_TOPC:def 5;
then the TopStruct of S = M|CS by A3,A4,PRE_TOPC:def 5;
then B is Basis of S by YELLOW12:32;
then weight S c= card B by WAYBEL23:73;
then weight S c= omega by A1,A2;
hence thesis by WAYBEL23:def 6;
end;
end;
registration
let M1,M2 be topological_manifold;
cluster [:M1,M2:] -> second-countable Hausdorff;
coherence;
end;~~