:: Topological Manifolds
:: by Karol P\kak
::
:: Received June 16, 2014
:: Copyright (c) 2014-2026 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, ORDINAL2;
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, BORSUK_1,
BORSUK_2, NAT_D, BINOP_1, EQREL_1, BORSUK_3, WAYBEL23, CANTOR_1,
METRIZTS;
constructors MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1, FUNCSDOM, BROUWER,
SEQ_4, EUCLID_9, SIMPLEX0, CONNSP_1, CONNSP_3, BORSUK_3, NAT_D, BORSUK_2,
WAYBEL23, CANTOR_1, REAL_1, METRIZTS;
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, 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, WAYBEL23;
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,
BORSUK_3, EUCLID_2, TOPREALA, FUNCT_3, EQREL_1, TIETZE_2, CONNSP_1,
CONNSP_3, CARD_2, WAYBEL23, YELLOW12, BROUWER3, JGRAPH_1, TOPS_4;
schemes FUNCT_2, NAT_1, CLASSES1;
begin :: Preliminaries
reserve n,m for Nat,
p,q for Point of TOP-REAL n, r for Real;
theorem Th1: :: MFOLD_1:1
for T being non empty TopSpace holds T , T | [#]T are_homeomorphic
proof
let X be non empty TopSpace;
set f = id X;
A1: dom f = [#]X;
A2: [#](X | ([#]X))= [#]X by PRE_TOPC:def 5;
A3: rng f = [#](X | ([#]X)) by PRE_TOPC:def 5;
reconsider XX=X|([#]X) as non empty TopSpace;
reconsider f as Function of X, XX by A2;
ZZ: for P being Subset of X st P is closed holds (f")"P is closed
proof
let P be Subset of X;
assume P is closed; then
A4: ([#]X) \ P in the topology of X by PRE_TOPC:def 2,def 3;
A5: for x being object holds x in (f")"P iff x in P
proof
let x be object;
hereby
assume A6: x in (f")"P;
x in f.:P by A6,A3,TOPS_2:54; then
consider y be object such that
A7: [y,x] in f & y in P by RELAT_1:def 13;
thus x in P by A7,RELAT_1:def 10;
end;
assume A8: x in P; then
[x,x] in id X by RELAT_1:def 10; then
x in f.:P by A8,RELAT_1:def 13;
hence x in (f")"P by A3,TOPS_2:54;
end;
S1: ([#]X) \ P = ([#] (X | ([#]X))) \ (f")"P by A2,A5,TARSKI:2;
([#]X) \ P = ([#]X /\ [#]X) \ P
.= (([#]X) \ P) /\ [#]X by XBOOLE_1:49; then
([#]X) \ P in the topology of (X | ([#]X)) by PRE_TOPC:def 4,
A2,A4; then
([#] (X | ([#]X))) \ (f")"P is open by PRE_TOPC:def 2,S1;
hence (f")"P is closed by PRE_TOPC:def 3;
end;
S0: f is continuous by JGRAPH_1:45;
f" is continuous by PRE_TOPC:def 6,ZZ; then
f is being_homeomorphism by A1,A3,TOPS_2:def 5,S0;
hence thesis by T_0TOPSP:def 1;
end;
definition
let n,p,r;
func Tball(p,r) -> SubSpace of TOP-REAL n equals
(TOP-REAL n) | Ball(p,r);
correctness;
end;
registration
let n, p;
let s be positive Real;
cluster Tball(p,s) -> non empty;
correctness;
end;
theorem :: MFOLD_1:4
the carrier of Tball(p,r) = Ball(p,r)
proof
[#]Tball(p,r) = Ball(p,r) by PRE_TOPC:def 5;
hence thesis;
end;
theorem Th3: ::MFOLD_1:9
for r,s being positive Real holds
Tball(p,r), Tball(q,s) are_homeomorphic
proof
set TR=TOP-REAL n;
let r,s be positive Real;
Ball(q,s) c= Int cl_Ball(q,s) by TOPREAL9:16,TOPS_1:24;
then A2: cl_Ball(q,s) is non boundary compact;
Ball(p,r) c= Int cl_Ball(p,r) by TOPREAL9: 16,TOPS_1:24;
then cl_Ball(p,r) is non boundary compact;
then consider h be Function of TR |cl_Ball(p,r),TR |cl_Ball(q,s) such that
A4: h is being_homeomorphism & h.:Fr cl_Ball(p,r) = Fr cl_Ball(q,s)
by A2,BROUWER2:7;
A5:[#](TR|cl_Ball(q,s))=cl_Ball(q,s) by PRE_TOPC:def 5;
A6:h.:(dom h) = rng h by RELAT_1:113
.= [#](TR|cl_Ball(q,s)) by FUNCT_2:def 3,A4;
A7: Fr cl_Ball(p,r) = Sphere(p,r) by BROUWER2:5;
A8:[#](TR|cl_Ball(p,r)) = cl_Ball(p,r) by PRE_TOPC:def 5;
A9:Ball(q,s) \/ Sphere(q,s) = cl_Ball(q,s) & Ball(q,s) misses Sphere(q,s)
by TOPREAL9:18,19;
A10:Ball(p,r) \/ Sphere(p,r) = cl_Ball(p,r)& Ball(p,r) misses Sphere(p,r)
by TOPREAL9:18,19;
reconsider Br=Ball(p,r) as Subset of TR |cl_Ball(p,r) by A10,A8,XBOOLE_1:7;
reconsider Bs=Ball(q,s) as Subset of TR |cl_Ball(q,s) by A9,A5,XBOOLE_1:7;
A12:dom h = [#] (TR|cl_Ball(p,r)) by FUNCT_2:def 1;
A13:Ball(q,s) \/ Sphere(q,s) = cl_Ball(q,s) &
Ball(q,s) misses Sphere(q,s) by TOPREAL9:18,19;
A14:Ball(p,r) \/ Sphere(p,r) = cl_Ball(p,r) &
Ball(p,r) misses Sphere(p,r) by TOPREAL9:18,19;
dom h \ Sphere(p,r) = Ball(p,r) by A12,A8,XBOOLE_1:88,A14;
then h.:Br = h.:(dom h) \ (Fr cl_Ball(q,s)) by A4,FUNCT_1:64,A7
.= cl_Ball(q,s) \ Sphere(q,s) by BROUWER2:5,A6,A5
.=Bs by A13,XBOOLE_1:88;
then TR |cl_Ball(p,r)|Br,TR |cl_Ball(q,s)|Bs are_homeomorphic
by A4,METRIZTS:3,METRIZTS:def 1;
then TR|Ball(p,r),TR|cl_Ball(q,s)|Bs are_homeomorphic by PRE_TOPC:7,A8;
hence thesis by PRE_TOPC:7,A5;
end;
registration
let n;
cluster TOP-REAL n -> second-countable;
correctness
proof
set TR=TOP-REAL n,T = the TopStruct of TR;
T=TR| [#]TR by TSEP_1:93;
then weight T = weight TR by Th1,METRIZTS:4;
hence thesis by WAYBEL23:def 6;
end;
end;
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;
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);
A12: n in NAT by ORDINAL1:def 12;
A13: CL c= Ball(hq,s) by A9,A12,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;
A20:dom h = [#]MU by A4,TOPS_2:def 5;
A21:h"W = IU by FUNCT_1:82,A4,FUNCT_1:76,A20;
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 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,A13,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 A13,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 :Def2:
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 :Def3:
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 non empty TopSpace;
func Int M -> Subset of M means :Def4:
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,Def4;
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 Def4,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
A5: M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def2;
A6: [#](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
A7: h is being_homeomorphism by T_0TOPSP:def 1,A5;
IU is open by TSEP_1:9;
then h.:IU is open by A7,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
A8: W in the topology of TR
and
A9: h.:IU = W/\[#]Tdisk(0.TR,1) by PRE_TOPC: def 4;
A10: [#]Tdisk(0.TR,1) = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
A11: dom h = [#]MU by A7,TOPS_2:def 5;
A12: Ball(0.TR,1) c= cl_Ball(0.TR,1) by TOPREAL9:16;
reconsider W as open Subset of TR by A8,PRE_TOPC:def 2;
set WB=W/\Ball(0.TR,1);
p in Int U by CONNSP_2:def 1;
then
A13: h.p in h.:IU by A11,FUNCT_1:def 6;
then
A14: h.p in W by A9,XBOOLE_0:def 4;
then reconsider hp=h.p as Point of TR;
A15: h .: IU = W/\cl_Ball(0.TR,1) by PRE_TOPC:def 5,A9;
WB is non empty
proof
reconsider HP=hp as Point of Euclid n by EUCLID:67;
A16: Ball(0.TR,1) misses Sphere(0.TR,1) by TOPREAL9:19;
A17: cl_Ball(0.TR,1) = Ball(0.TR,1)\/Sphere(0.TR,1) by TOPREAL9:18;
assume
A18: 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 A16,A17,XBOOLE_1:88;
then hp in Sphere(0.TR,1) by A15,A13,XBOOLE_0:def 4;
then
A19: |.hp.| = 1 by TOPREAL9:12;
Int W=W by TOPS_1:23;
then consider s be Real such that
A20: s>0
and
A21: Ball(HP,s) c= W by A14,GOBOARD6:5;
set s2=s/2,m=min(s/2,1/2);
A22: m <=s2 by XXREAL_0:17;
s2 <s by A20,XREAL_1:216;
then
A23: m < s by A22,XXREAL_0:2;
A24: Ball(HP,s)=Ball(hp,s) by TOPREAL9:13;
A25: m >0 by A20,XXREAL_0:21;
then
A26: 1-m < 1-0 by XREAL_1:6;
A27: |. -m .|=--m by A25,ABSVALUE:def 1;
A28: (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 A19,EUCLID:11;
then
A29: ( 1-m)*hp in Ball(hp,s) by A27,A23;
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 A19,EUCLID:11;
then (1-m)*hp in Ball(0.TR,1) by A28,A26;
hence thesis by A29,A21,A24,A18,XBOOLE_0:def 4;
end;
then consider wb be set such that
A30: wb in WB;
reconsider wb as Point of TR by A30;
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
A31: s>0
and
A32: Ball(wbE,s) c= WB by A30,GOBOARD6:5;
A33:Ball(wb,s)=Ball(wbE,s) by TOPREAL9:13;
WB c= Ball(0.TR,1) by XBOOLE_1:17;
then
A34: Ball(wb,s) c= Ball(0.TR,1) by A32,A33;
then
reconsider BB=Ball(wb,s) as Subset of Tdisk(0.TR,1) by A12,XBOOLE_1:1,A10;
A35: Tdisk(0.TR,1) | BB = TR|Ball(wb,s) by A34,A12,XBOOLE_1:1,PRE_TOPC:7;
reconsider hBB=h"BB as Subset of M by A6,XBOOLE_1:1;
BB is open by TSEP_1:9;
then
A36:h"BB is open by A7,TOPGRP_1:26;
WB c= h .: IU by A10,A9,TOPREAL9:16,XBOOLE_1:26;
then BB c= h.:IU by A32,A33;
then
A37: h"BB c= h"(h.:IU) by RELAT_1:143;
h"(h.:IU)c= IU by FUNCT_1:82,A7;
then h"BB c= IU by A37;
then hBB is open by A36,TSEP_1:9;
then
A38: Int hBB = hBB by TOPS_1:23;
A39: rng h = [#]Tdisk(0.TR,1) by A7,TOPS_2:def 5;
then
A40: h.:(h"BB)=BB by FUNCT_1:77;
hBB is non empty by A31,RELAT_1:139,A39;
then consider t be set such that
A41: t in hBB;
reconsider t as Point of M by A41;
reconsider hBB as a_neighborhood of t by A38,CONNSP_2:def 1,A41;
A43: MU|h"BB =M|hBB by A6,PRE_TOPC:7;
then reconsider HH=h|h"BB as Function of M|hBB,TR|Ball(wb,s)
by A40,A35,JORDAN24:12;
HH is being_homeomorphism by A7,A40,A35,A43,METRIZTS:2;
then
A44:M|hBB,TR|Ball(wb,s) are_homeomorphic by T_0TOPSP:def 1;
Tball(wb,s), Tball(0.TR,1) are_homeomorphic by Th3,A31;
then M|hBB,Tball(0.TR,1) are_homeomorphic by A44,A31,BORSUK_3:3;
hence thesis by A1,TOPS_1:25,Def4;
end;
end;
definition
let M be non empty TopSpace;
func Fr M -> Subset of M equals (Int M)`;
coherence;
end;
::$N Boundary Points of Locally Euclidean Spaces
theorem Th5:
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 Def2;
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;
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,Th3;
then M|HW, Tball(0.TR,1) are_homeomorphic by A27,A17,BORSUK_3:3;
then p in Int M by Def4;
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 Def4;
A33: 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,A33,XBOOLE_0:3,BROUWER3:15,A31;
then consider g be Function of M|W,TR|Ball(0.TR,1) such that
A34: g is being_homeomorphism by A31,T_0TOPSP:def 1;
A35: Int U c= U by TOPS_1:16;
set I = (Int U)/\Int W;
A36: [#](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,A35,A36,A30,A33,XBOOLE_0:def 4,TSEP_1:9;
A37: dom h = [#](M|U) by A28,TOPS_2:def 5;
then
A38: h"(h.:IU) = IU by A28,FUNCT_1:94;
p in I by A30,A33,XBOOLE_0:def 4;
then
A39: h.p in h.:IU by A37,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
A40: Q in the topology of TR
and
A41: h.:IU = Q /\[#](TR|cl_Ball(0.TR,1)) by PRE_TOPC: def 4;
reconsider Q as non empty Subset of TR by A41;
A42: Int Q=Q by A40,PRE_TOPC:def 2,TOPS_1:23;
A43: I c= Int W by XBOOLE_1:17;
A44: [#] (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 A39;
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 A39,A41,XBOOLE_0:def 4;
then consider s be Real such that
A45: s>0
and
A46: Ball(HP,s) c= Q by A42,GOBOARD6:5;
set s2=s/2;
hp is Element of REAL n by EUCLID:22;
then |. hp-hp .|=0;
then
A47:hp in Ball(hp,s2) by A45;
set clb = cl_Ball(hp,s2)/\cl_Ball(0.TR,1);
A48: 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 A48,A47,A39,XBOOLE_0:def 4;
A49: 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;
A50:Ball(HP,s)=Ball(hp,s) by TOPREAL9:13;
hp in CLB by A48,A47,A39,A44,XBOOLE_0:def 4;
then
A51: p in hCLB by A37,A36,A35,A30,FUNCT_1:def 7;
n in NAT by ORDINAL1:def 12;
then
A52: cl_Ball(hp,s2) c= Ball(hp,s) by XREAL_1:216,A45,JORDAN:21;
then cl_Ball(hp,s2) c= Q by A46,A50;
then CLB c= h.:IU by A44,XBOOLE_1:26,A41;
then
A53: hCLB c= IU by RELAT_1:143,A38;
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 A36,XBOOLE_1:1;
Ball(hp,s2) c= Q by A46,A50,A48,A52;
then BB c= h.:IU by XBOOLE_1:26,A41;
then
A54: h"BB c= IU by RELAT_1: 143,A38;
reconsider HCLB=hCLB as non empty Subset of M by A36,XBOOLE_1:1;
A55: h.:hCLB = CLB by A49,FUNCT_1:77;
A56:(TR|cl_Ball(0.TR,1)) |CLB = TR|clb by A44,PRE_TOPC:7;
A57:(M|U) |hCLB = M|HCLB by A36,PRE_TOPC:7;
then reconsider h1=h|hCLB as Function of M|HCLB,TR|clb
by A56,A55,JORDAN24:12;
A58: Int W c= W by TOPS_1:16;
A59: [#](M|W)=W by PRE_TOPC:def 5;
then reconsider IW = I as non empty open Subset of (M|W)
by A30,A33,XBOOLE_0:def 4,XBOOLE_1:1,A58,A43,TSEP_1:9;
A60: IU c= W by A58,A43;
then reconsider hCLW=hCLB as non empty Subset of M|W by A53,XBOOLE_1:1,A59;
A61:(M|W) |hCLW = M|HCLB by A53,A60,XBOOLE_1:1,PRE_TOPC:7;
set ghCLW = g.:hCLW;
A62: [#] (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;
A63:(TR|Ball(0.TR,1)) | ghCLW = TR|GhCLW by A62,PRE_TOPC:7;
then reconsider g1=g|hCLB as Function of M|HCLB,TR|GhCLW by A61,JORDAN24:12;
A64:g1 is being_homeomorphism by A34,METRIZTS:2,A63,A61;
then
A65:g1" is being_homeomorphism by TOPS_2:56;
A66: dom g = [#](M|W) by A34,TOPS_2:def 5;
then g.p in GhCLW by A51,FUNCT_1:def 6;
then reconsider gp=g.p as Point of TR;
I c= W by A58,A43;
then reconsider hBW=hBB as Subset of (M|W) by A54,XBOOLE_1:1,A59;
reconsider ghBW=g.:hBW as Subset of TR by A62,XBOOLE_1:1;
hp in BB by A47,A39,XBOOLE_0:def 4;
then p in h"BB by A37,A36,A35,A30,FUNCT_1:def 7;
then
A67:gp in ghBW by A66,FUNCT_1:def 6;
set hg= h1*(g1");
h1 is being_homeomorphism by A28,A56,METRIZTS:2,A57,A55;
then
A68:hg is being_homeomorphism by A65,TOPS_2:57;
then
A69: dom hg = [#](TR|GhCLW) by TOPS_2:def 5;
BB c= clb by TOPREAL9:16,XBOOLE_1:26,A44;
then
A70: hBB c= hCLB by RELAT_1:143;
then ghBW c= GhCLW by RELAT_1:123;
then gp in GhCLW by A67;
then
A71:gp in dom hg by A69,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 A47,A39,XBOOLE_0:def 4,PRE_TOPC:def 2;
then h"BB is open by A28,TOPGRP_1:26;
then hBB is open by A54,TSEP_1:9;
then hBW is open by TSEP_1:9;
then g.:hBW is open by A34,TOPGRP_1:25;
then ghBW is open by A62,TSEP_1:9;
then gp in Int GhCLW by A67,TOPS_1:22,A70,RELAT_1:123;
then
A72: hg.gp in Int clb by BROUWER3:11,A68;
Int clb = (Int cl_Ball(hp,s2)) /\ Int cl_Ball(0.TR,1) by TOPS_1:17;
then
A73: hg.gp in Int cl_Ball(0.TR,1) by A72,XBOOLE_0:def 4;
reconsider G1=g1 as Function;
Fr cl_Ball(0.TR,1) = Sphere(0.TR,1) by BROUWER2:5;
then
A74:Int cl_Ball(0.TR,1) = cl_Ball(0.TR,1)\Sphere(0.TR,1) by TOPS_1:40;
A75:G1"=g1" by A64,TOPS_2:def 4;
dom g1 = [#](M|HCLB) by A64,TOPS_2:def 5;
then p in dom g1 by PRE_TOPC:def 5,A51;
then
A76: (g1".(g1.p)) = p by A64,A75,FUNCT_1:34;
A77:g.p = g1.p by A51, FUNCT_1:49;
then
A78: p in dom h1 by A71,FUNCT_1:11,A76;
hg.gp = h1.p by A71,FUNCT_1:12,A76,A77;
then hg.gp = h.p by A78,FUNCT_1:47;
hence contradiction by A29, A73,A74,XBOOLE_0:def 5;
end;
begin :: Interior and Boundary of Locally Euclidean Spaces
definition
let M be non empty TopSpace;
attr M is without_boundary means :Def6:
Int M = the carrier of M;
end;
notation
let M be non empty TopSpace;
antonym M is with_boundary for M is without_boundary;
end;
Lm2: (M is locally_euclidean 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 without_boundary;
let p be Point of M;
consider U be a_neighborhood of p,n such that
A2: 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
A3: h is being_homeomorphism by A2,T_0TOPSP:def 1;
A4: cl_Ball(0.TR,1) = Ball(0.TR,1) \/ Sphere(0.TR,1) by TOPREAL9:18;
A5: [#]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;
A6: [#]MU = U by PRE_TOPC:def 5;
then reconsider IU=Int U as Subset of M|U by TOPS_1:16;
A7: 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 A5,XBOOLE_1:1;
A8: HIB c= Ball(0.TR,1) by XBOOLE_1:17;
IU is open by TSEP_1:9;
then h.:(Int U) is open by A3,TOPGRP_1:25;
then
A9: hib is open by TSEP_1:9,A8;
reconsider MM=M as locally_euclidean non empty TopSpace by A1;
A10: Int U c= U by TOPS_1:16;
A11: dom h = [#]MU by A3,TOPS_2:def 5;
then
A12: h.p in rng h by A7,A10,A6,FUNCT_1:def 3;
A13: h.p in Ball(0.TR,1)
proof
assume not h.p in Ball(0.TR,1);
then
A14: h.p in Sphere(0.TR,1) by A5,A12,A4,XBOOLE_0:def 3;
Fr MM = (the carrier of MM) \ Int MM by SUBSET_1:def 4
.={} by XBOOLE_1:37,A1;
hence contradiction by A14,A3,Th5;
end;
then reconsider hP=h.p as Point of TR;
h.p in h.:(Int U) by A7,A10,A6,A11,FUNCT_1:def 6;
then h.p in hib by A13,XBOOLE_0:def 4;
then consider r be positive Real such that
A15: Ball(hP,r) c= hib by A9,TOPS_4:2;
|.hP-hP.|=0 by TOPRNS_1:28;
then A16:hP in Ball(hP,r);
reconsider bb=Ball(hP,r) as non empty Subset of Tdisk(0.TR,1)
by A15,XBOOLE_1:1;
reconsider hb=h"bb as Subset of M by A6,XBOOLE_1:1;
bb is open by TSEP_1:9;
then
A17: h"bb is open by A3,TOPGRP_1:26;
A18: h"HIB c= h"(h.:Int U) by XBOOLE_1:17,RELAT_1:143;
A19: h"(h.:Int U) c= Int U by A3,FUNCT_1:82;
A20: M|hb = M|U | (h"bb) by A6,PRE_TOPC:7;
hb c= h"HIB by A15,RELAT_1:143;
then hb c= Int U by A18,A19;
then
A21: hb is open by A6,TSEP_1:9,A17,A10;
p in hb by A16, A7,A10,A6,A11,FUNCT_1:def 7;
then
A22: p in Int hb by A21,TOPS_1:23;
rng h = [#]Tdisk(0.TR,1) by A3,TOPS_2:def 5;
then
A23: h.: (h"bb) = bb by FUNCT_1:77;
A25: Tdisk(0.TR,1) | bb = TR|Ball(hP,r) by A5, PRE_TOPC:7;
then reconsider hh=h| (h"bb) as Function of M|hb,Tball(hP,r)
by A20,JORDAN24:12,A23;
reconsider hb as a_neighborhood of p by A22,CONNSP_2:def 1;
hh is being_homeomorphism by A3,A20,A23, A25,METRIZTS:2;
then
A26: M|hb,Tball(hP,r) are_homeomorphic by T_0TOPSP:def 1;
take hb;
take n;
Tball(hP,r),Tball(0.TR,1) are_homeomorphic by Th3;
hence M|hb,Tball(0.TOP-REAL n,1) are_homeomorphic by A26,BORSUK_3:3;
end;
assume
A27: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
A28: M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A27;
set En=Euclid n;
set TR=TOP-REAL n;
A29: 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
A30: h is being_homeomorphism by A28,T_0TOPSP:def 1;
A31: n in NAT by ORDINAL1:def 12;
A33: [#]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,A31;
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 A33,XBOOLE_1:1;
A35: dom h = [#]MU by A30,TOPS_2:def 5;
then
A36: IU=h"hIU by A30,FUNCT_1:82,FUNCT_1:76;
A37: the TopStruct of TR = TopSpaceMetr En by EUCLID:def 8;
then reconsider hIUE=hIU as Subset of TopSpaceMetr En;
A38: p in Int U by CONNSP_2:def 1;
then
A39: h.p in hIU by A35,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 A39;
IU is open by TSEP_1:9;
then h.:IU is open by A30,TOPGRP_1:25;
then hIU is open by A33,TSEP_1:9;
then hIU in the topology of TR by PRE_TOPC:def 2;
then consider r be Real such that
A40: r > 0
and
A41: Ball(hp,r) c= hIUE by A39,A37,PRE_TOPC:def 2,TOPMETR:15;
set r2=r/2;
A42: Ball(Hp,r)=Ball(hp,r) by TOPREAL9:13;
cl_Ball(Hp,r2) c= Ball(Hp,r) by A31,XREAL_1:216,A40,JORDAN:21;
then
A43: cl_Ball(Hp,r2) c= hIU by A41,A42;
then reconsider CL=cl_Ball(Hp,r2) as Subset of Tball(0.TR,1)
by XBOOLE_1:1;
A44: cl_Ball(Hp,r2) c= [#]Tball(0.TR,1) by A43,XBOOLE_1:1;
then cl_Ball(Hp,r2) c= rng h by A30,TOPS_2:def 5;
then
A45: h.:(h"CL) = CL by FUNCT_1:77;
set r22=r2/2;
r22 < r2 by A40,XREAL_1:216;
then
A46: Ball(Hp,r22) c= Ball(Hp,r2) by A31,JORDAN:18;
reconsider hCL=h"CL as Subset of M by A34,XBOOLE_1:1;
A47: (M|U) | (h"CL) = M| hCL by A34,PRE_TOPC:7;
A48: Ball(Hp,r2) c= cl_Ball(Hp,r2) by TOPREAL9:16;
then
A49: Ball(Hp,r22) c= cl_Ball(Hp,r2) by A46;
then reconsider BI = Ball(Hp,r22) as Subset of Tball(0.TR,1)
by A44,XBOOLE_1:1;
BI c= hIU by A43, A48,A46;
then
A50: 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 A30,TOPGRP_1:26;
then
A51: hBI is open by A36,A50,TSEP_1:9;
|.Hp - Hp.|=0 by TOPRNS_1:28;
then h.p in BI by A40;
then p in h"BI by A38,A29,A34,A35,FUNCT_1:def 7;
then p in Int hCL by A49,RELAT_1:143,TOPS_1:22,A51;
then reconsider hCL as a_neighborhood of p by CONNSP_2:def 1;
A52: Tball(0.TR,1) |CL = Tdisk(Hp,r2) by A33,PRE_TOPC:7;
then reconsider hh=h| (h"CL) as Function of M|hCL,Tdisk(Hp,r2)
by A45,JORDAN24:12,A47;
hh is being_homeomorphism by A30,A52,METRIZTS:2,A45,A47;
then
A53: M|hCL,Tdisk(Hp,r2) are_homeomorphic by T_0TOPSP:def 1;
Tdisk(Hp,r2),Tdisk(0.TR,1) are_homeomorphic by Lm1, A40;
hence thesis by A53,BORSUK_3:3,A40;
end;
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,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A27;
hence thesis by Def4;
end;
Lm3:
Tball(0.TOP-REAL n,1) is n-locally_euclidean 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;
thus thesis by TSEP_1:93;
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;
A5: p in Int U by CONNSP_2:def 1;
consider W be a_neighborhood of p,m such that
A6: MM|W,Tdisk(0.TOP-REAL m,1) are_homeomorphic by Def2;
p in Int W by CONNSP_2:def 1;
then m=n by A5,XBOOLE_0:3,A3,A6,BROUWER3:15;
hence thesis by A6;
end;
hence thesis by A2,Lm2;
end;
registration
let n;
cluster Tball(0.TOP-REAL n,1) -> without_boundary n-locally_euclidean;
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,Th5;
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 Def6
.={} 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,Def6;
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, Th5;
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 Def3;
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 by Lm2;
theorem Th7:
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, Th5;
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,Th5,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;
A37:[#] (TR|CL) = CL by PRE_TOPC:def 5;
then reconsider hFIU=h.:FIU as Subset of TR by XBOOLE_1:1;
A38:[#](TR|hFIU)=hFIU by PRE_TOPC:def 5;
A39:Tdisk(0.TR,1) | (h.:FIU) = TR|hFIU by A37,PRE_TOPC:7;
then reconsider hfiu=h|FIU as Function of Mfiu, TR|hFIU by JORDAN24:12;
A40: hfiu is being_homeomorphism by A9,A6,METRIZTS:2,A39;
A41:Ball(0.TR1,1) misses Sphere(0.TR1,1) by TOPREAL9:19;
A42: S c= CL by TOPREAL9:17;
A43: IU = h"(h.:IU) by FUNCT_1:82,A6,FUNCT_1:76,A16;
V0 c= Ball(hp,m) by XBOOLE_1:17;
then
A44: V0 c= W by A21,A23,A24;
A45: 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 A44,A46,A15,A42,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;
A50: V0 c= S by XBOOLE_1:17;
then V0 c= CL by A42;
then V0 c= h.:IU by A44,A14,XBOOLE_1:19, A37;
then
A51: hV0 c= IU by A43,RELAT_1:143;
A52: rng h = [#]Tdisk(0.TR,1) by A9,A6, TOPS_2:def 5;
then h.:(h"V0) = V0 by FUNCT_1:77, A42,A50,XBOOLE_1:1,A37;
then
A53: Tdisk(0.TR,1) | (h.:(h"V0)) = TR |V0 by PRE_TOPC:7,A42,A50,XBOOLE_1:1;
A54:CL=S\/Ball(0.TR,1) by TOPREAL9:18;
A55: hFIU /\ Ball(hp,m) c= V0
proof
let x be object;
assume
A56: x in hFIU /\ Ball(hp,m);
then reconsider q=x as Point of TR;
A57: x in hFIU by A56,XBOOLE_0:def 4;
A58: q in S
proof
reconsider Q=q as Point of Euclid n1 by EUCLID:67;
set WB=W/\Ball(0.TR,1);
A59: Int WB=WB by TOPS_1:23;
hFIU c= h.:IU by XBOOLE_1:17,RELAT_1:123;
then
A60: q in W by A57,A14,XBOOLE_0:def 4;
assume not q in S;
then q in Ball(0.TR,1) by A57, A37,A54,XBOOLE_0:def 3;
then q in WB by A60,XBOOLE_0:def 4;
then consider w be Real such that
A61: w>0
and
A62: Ball(Q,w) c= WB by A59,GOBOARD6:5;
set B=Ball(q,w);
A63: Ball(Q,w)=Ball(q,w) by TOPREAL9:13;
consider u be object such that
A64: u in dom h
and
A65: u in FIU
and
A66: h.u=q by FUNCT_1:def 6,A57;
reconsider u as Point of M by A65;
A67: Ball(0.TR,1) c= CL by A54, XBOOLE_1:11;
WB c= Ball(0.TR,1) by XBOOLE_1:17;
then
A68: B c= Ball(0.TR,1) by A62,A63;
then reconsider BB=B as Subset of Tdisk(0.TR,1) by A67,XBOOLE_1:1,A37;
reconsider hBB=h"BB as Subset of M by A12,XBOOLE_1:1;
A69: B in the topology of TR by PRE_TOPC:def 2;
|.q-q.|=0 by TOPRNS_1:28;
then q in BB by A61;
then
A70: u in hBB by A64,A66,FUNCT_1:def 7;
BB /\CL =BB by A67,XBOOLE_1:1,A68,XBOOLE_1:28;
then BB in the topology of Tdisk(0.TR,1) by A69,A37,PRE_TOPC:def 4;
then BB is open by PRE_TOPC:def 2;
then
A72: h"BB is open by TOPGRP_1:26,A9,A6;
WB c= W by XBOOLE_1:17;
then BB c= W by A62,A63;
then BB c= h.:IU by XBOOLE_1:19,A14;
then h"BB c= Int U by RELAT_1:143,A43;
then hBB is open by A10,A12,A72,TSEP_1:9;
then
A73: Int hBB = hBB by TOPS_1:23;
A74: Tdisk(0.TR,1) | BB = TR|Ball(q,w) by A37,PRE_TOPC: 7;
reconsider hBB as a_neighborhood of u by A73,A70,CONNSP_2:def 1;
A75: h.:hBB =BB by FUNCT_1:77,A52;
A76: 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,A74,A75;
hB is being_homeomorphism by A9,A6,A74,A75,A76,METRIZTS:2;
then
A77: M|hBB,Tball(q,w) are_homeomorphic by T_0TOPSP:def 1;
Tball(q,w),Tball(0.TR,1) are_homeomorphic by A61,Th3;
then M|hBB,Tball(0.TR,1) are_homeomorphic by A77,A61,BORSUK_3:3;
then
A78: u in Int M by Def4;
u in F by A65,XBOOLE_0:def 4;
then u in [#]M \ Int M by SUBSET_1:def 4;
hence thesis by XBOOLE_0:def 5,A78;
end;
x in Ball(hp,m) by A56,XBOOLE_0:def 4;
hence thesis by A58,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
A79: hFIU /\ Ball(hp,m) = V0 by A55,XBOOLE_1:26,A45;
reconsider v0=V0 as Subset of TR|hFIU by A38,A45;
Ball(hp,m) in the topology of TR by PRE_TOPC:def 2;
then v0 in the topology of TR|hFIU by A79,PRE_TOPC:def 4,A38;
then
A80: v0 is open by PRE_TOPC:def 2;
A81:Ball(0.TR1,1) \/ Sphere(0.TR1,1) = cl_Ball(0.TR1,1) by TOPREAL9:18;
A83: |. hp - 0.TR.| = |. 0.TR - hp.| by TOPRNS_1:27;
A84:m>0 by A20,XXREAL_0:21;
then
A85: |.0.TR - hp.| < 1+m by A19,A83,XREAL_1:29;
|.hp-hp.|=0 by TOPRNS_1:28;
then hp in Ball(hp,m) by A84;
then
A86:hp in V0 by A9,A7,XBOOLE_0:def 4;
A87: pF in Int U by A4,CONNSP_2:def 1;
then
A88: pF in hV0 by A16,A10,A12,A4,A86,FUNCT_1:def 7;
m <= 1/2 by XXREAL_0:17;
then m < |.0.TR - hp.| by A19,A83,XXREAL_0:2;
then
consider g be Function of TR | (S /\ cl_Ball(hp,m)),Tdisk(0.TR1,1) such that
A89: g is being_homeomorphism
and
A90: g.:(S /\ Sphere(hp,m)) = Sphere(0. TR1,1) by A19,A83,A85,BROUWER3:19;
A91:(g.:S) /\ (g.:Ball(hp,m)) = g.:V0 by A89,FUNCT_1:62;
A92: [#]Mfiu = FIU by PRE_TOPC:def 5;
then reconsider U0=hV0 as non empty Subset of Mfiu
by A51,A25,XBOOLE_1:19,A16,A87,A4,A86,FUNCT_1:def 7;
reconsider U0 = hV0 as Subset of Mfiu by A51,A25,XBOOLE_1:19,A92;
A93:[#](MF|FIU1)=FIU by PRE_TOPC:def 5;
then reconsider u0=U0 as Subset of MF|FIU1 by A92;
hfiu"v0 = FIU /\ U0 by FUNCT_1:70;
then hfiu"v0 = U0 by A51,A25,XBOOLE_1:19,XBOOLE_1:28;
then
A94: U0 is open by A80,A40,TOPGRP_1:26;
reconsider FV0=u0 as Subset of MF by XBOOLE_1:1,A92;
A95: 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,A94,TSEP_1:9,A93;
then pF in Int FV0 by A88,TOPS_1:22;
then reconsider FV0 as a_neighborhood of pF by CONNSP_2:def 1;
reconsider MV0=FV0 as Subset of M by A51,XBOOLE_1:1;
hV0 c= IU/\F by A51,A25,XBOOLE_1:19;
then FV0 c= F/\U by A95;
then
A96: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
A97:Sphere(0. TOP-REAL n,1) misses g.:V0 by A89,A90,FUNCT_1:66;
A98:((g.:S) /\ (g.:Sphere(hp,m))) = g.:(S/\Sphere(hp,m)) by A89,FUNCT_1:62;
A99: [#](TR| (S /\ cl_Ball(hp,m))) = S /\ cl_Ball(hp,m) by PRE_TOPC:def 5;
then
A100: dom g = S /\ cl_Ball(hp,m) by A89,TOPS_2:def 5;
A101: 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,A99;
A102: g.:cl_Ball(hp,m) = (g.:Ball(hp,m)) \/ (g.:Sphere(hp,m))
by A101,RELAT_1:120;
A103: [#](Tdisk(0.TR1,1)) = cl_Ball(0.TR1,1) by PRE_TOPC:def 5;
then rng g = cl_Ball(0.TR1,1) by A89,TOPS_2:def 5;
then cl_Ball(0.TR1,1) = g.:(S /\ cl_Ball(hp,m)) by A100,RELAT_1:113
.= (g.:S) /\ (g.:cl_Ball(hp,m)) by A89,FUNCT_1:62
.= (g.:V0) \/ Sphere(0.TOP-REAL n,1)
by A102,A98,A91,A90,XBOOLE_1:23;
then g.:V0 = Ball(0.TR1,1) by A81,A41,A97,XBOOLE_1:71;
then
A104: Tdisk(0.TR1,1) | (g.:ZV0) = Tball(0.TR1,1) by PRE_TOPC:7,A103;
A105:TR | (S /\ cl_Ball(hp,m)) | ZV0 = TR|V0 by A99,PRE_TOPC:7;
then reconsider GG=g|ZV0 as Function of TR | V0,Tball(0.TR1,1)
by A86,JORDAN24:12,A104;
A106: GG is being_homeomorphism by A89,METRIZTS:2,A105,A104;
A107: M|MV0 = MF|FV0 by A5,PRE_TOPC:7;
then reconsider HH=h|FV0 as Function of MF|FV0,TR|V0
by A96,A53,JORDAN24:12;
reconsider GH=GG*HH as Function of MF |FV0,Tball(0.TR1,1) by A86;
take FV0;
HH is being_homeomorphism by A9,A6,METRIZTS:2,A96,A53,A107;
then GH is being_homeomorphism by A86,A106,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,Def4;
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) = 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,A10;
then
A11: Int hum = hum by TOPS_1:23;
A12: h"(h.:UIM) c= UIM by A6,FUNCT_1:82;
A13: q in Int U by CONNSP_2:def 1;
then
A14: 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 A14,A8,FUNCT_1:def 6;
then consider s be Real such that
A15: s>0
and
A16: Ball(HQ,s) c= hum by A11,GOBOARD6:5;
A17:Ball(HQ,s)=Ball(hq,s) by TOPREAL9:13;
then reconsider BB=Ball(hq,s) as Subset of Tball(0.TR,1) by A16,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 A16,A17,RELAT_1:143;
then
A18: hBB c= UIM by A12;
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 A18,XBOOLE_1:1,A1;
hBBM is open by TSEP_1:9,A18;
then
A19:HBB is open by TSEP_1:9;
A20: 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
A21:Tball(0.TR,1) | (h.:hBB) = TR|Ball(hq,s) by A10,PRE_TOPC:7;
|.hq-hq.|=0 by TOPRNS_1:28;
then hq in BB by A15;
then p in HBB by FUNCT_1:def 7,A13,A3,A8,A7;
then p in Int HBB by A19,TOPS_1:23;
then reconsider HBB as a_neighborhood of p by CONNSP_2:def 1;
A22: MU|hBB =M|hBBM by A7,PRE_TOPC:7;
then reconsider hh=h|hBB as Function of MI|HBB,TR|Ball(hq,s)
by A21,JORDAN24:12,A20;
hh is being_homeomorphism by A6,A21,A22,A20,METRIZTS:2;
then
A23: MI|HBB,Tball(hq,s) are_homeomorphic by T_0TOPSP:def 1;
take HBB;
Tball(hq,s),Tball(0.TR,1) are_homeomorphic by A15,Th3;
hence thesis by A15,A23,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 Th7,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 Th5, 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 Th5,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 Def2;
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 Def2;
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 Th8:
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 Def2;
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 Th5;
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
A24: [: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,A24,A12,ZFMISC_1:87;
end;
then p in Fr NM by A21,A4,Th5,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 Th5;
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 Def2;
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
A47: [: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,A47,A35,ZFMISC_1:87;
end;
then p in Fr NM by A44,A4,Th5,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,Def4;
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,Def4;
reconsider p=z as Point of NM by A53;
set TRn=TOP-REAL n,TRm=TOP-REAL m;
reconsider mn=m+n as Nat;
[:N|U,M|W:], (TOP-REAL mn) | Ball(0.TOP-REAL mn,1)
are_homeomorphic by A57,A58,TIETZE_2:20;
then NM| [:U,W:],Tball(0.TOP-REAL mn,1) are_homeomorphic
by BORSUK_3:22;
hence thesis by Def4, A56;
end;
theorem Th9:
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 Th8
.= [:([#]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 Th8
.= [:the carrier of N,Int M:] by Def6
.= [:the carrier of N,the carrier of M:] by Def6
.= 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 Th9;
hence thesis;
end;
cluster [:M,N:] -> with_boundary;
coherence
proof
Fr [:M,N:] = [: [#]M,Fr N:] \/ [: Fr M,[#]N:] by Th9;
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 :Def7: :: redefines Int (MFOLD_0, definition)
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 Def3;
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,Def4;
p in Int U by CONNSP_2:def 1;
then n=m by A3,XBOOLE_0:3,A4,A2,BROUWER3:15;
hence thesis by A4;
end;
thus thesis by Def4,A1;
end;
assume
A6: 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
A7: 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 A7,A6;
hence thesis by Def4;
end;
let x be object;
assume
A8: x in Int M;
then reconsider x as Point of M;
consider U be a_neighborhood of x, m such that
A9: M|U,Tball(0.TOP-REAL m,1) are_homeomorphic by A8,Def4;
consider W be a_neighborhood of x such that
A11: M|W,Tdisk(0.TOP-REAL n,1) are_homeomorphic by Def3;
A12: x in Int W by CONNSP_2:def 1;
x in Int U by CONNSP_2:def 1;
then m=n by A12,XBOOLE_0:3,BROUWER3:15,A9,A11;
hence thesis by A6,A9;
end;
coherence;
end;
definition
let n;
let M be n-locally_euclidean non empty TopSpace;
redefine func Fr M -> Subset of M means :: redefines Fr (MFOLD_0, definition)
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 Def3;
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,Th5;
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 Th5,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 Th5;
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,Th5;
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 Def3;
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 Th11:
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 Th13:
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 Def3,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;
A8: 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,Th5;
hence contradiction;
end;
then reconsider hP=h.p as Point of TR;
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 r be positive Real such that
A16: Ball(hP,r) c= hib by A15,TOPS_4:2;
|.hP-hP.|=0 by TOPRNS_1:28;
then A17:hP in Ball(hP,r);
reconsider bb=Ball(hP,r) as non empty Subset of Tdisk(0.TR,1)
by A16,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,A8;
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;
rng h = [#]Tdisk(0.TR,1) by A3,TOPS_2:def 5;
then
A22: h.: (h"bb) = bb by FUNCT_1:77;
A24: Tdisk(0.TR,1) | bb = TR|Ball(hP,r) by A4,PRE_TOPC:7;
then reconsider hh=h| (h"bb) as Function of M|hb,Tball(hP,r)
by A19,JORDAN24:12,A22;
reconsider hb as a_neighborhood of p by A21,CONNSP_2:def 1;
hh is being_homeomorphism by A3,A19,A22,A24,METRIZTS:2;
then
A25: M|hb,Tball(hP,r) are_homeomorphic by T_0TOPSP:def 1;
take hb;
Tball(hP,r),Tball(0.TR,1) are_homeomorphic by Th3;
hence M|hb,Tball(0.TR,1) are_homeomorphic by A25,BORSUK_3:3;
end;
assume
A26: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
A27: M|U,Tball(0.TR,1) are_homeomorphic by A26;
A28: n in NAT by ORDINAL1:def 12;
A30: [#]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,A28;
set MU=M|U;
consider h be Function of MU,Tball(0.TR,1) such that
A31: h is being_homeomorphism by A27,T_0TOPSP:def 1;
set En=Euclid n;
A32: Int U c= U by TOPS_1:16;
A33: [#]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 A30,XBOOLE_1:1;
A34: dom h = [#]MU by A31,TOPS_2:def 5;
then
A35: IU=h"hIU by A31,FUNCT_1:82,FUNCT_1:76;
A36:the TopStruct of TR = TopSpaceMetr En by EUCLID:def 8;
then reconsider hIUE=hIU as Subset of TopSpaceMetr En;
A37:p in Int U by CONNSP_2:def 1;
then
A38: h.p in hIU by A34,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 A38;
IU is open by TSEP_1:9;
then h.:IU is open by A31,TOPGRP_1:25;
then hIU is open by A30,TSEP_1:9;
then hIU in the topology of TR by PRE_TOPC:def 2;
then consider r be Real such that
A39: r > 0
and
A40: Ball(hp,r) c= hIUE by A38,A36,PRE_TOPC:def 2,TOPMETR:15;
set r2=r/2;
A41: Ball(Hp,r)=Ball(hp,r) by TOPREAL9:13;
cl_Ball(Hp,r2) c= Ball(Hp,r) by A28,XREAL_1:216,A39,JORDAN:21;
then
A42: cl_Ball(Hp,r2) c= hIU by A40,A41;
then
reconsider CL=cl_Ball(Hp,r2) as Subset of Tball(0.TR,1) by XBOOLE_1:1;
A43: cl_Ball(Hp,r2) c= [#]Tball(0.TR,1) by A42,XBOOLE_1:1;
then cl_Ball(Hp,r2) c= rng h by A31,TOPS_2:def 5;
then
A44: h.:(h"CL) = CL by FUNCT_1:77;
set r22=r2/2;
r22 < r2 by A39,XREAL_1:216;
then
A45: Ball(Hp,r22) c= Ball(Hp,r2) by A28,JORDAN:18;
reconsider hCL=h"CL as Subset of M by A33,XBOOLE_1:1;
A46: (M|U) | (h"CL) = M| hCL by A33,PRE_TOPC:7;
A47: Ball(Hp,r2) c= cl_Ball(Hp,r2) by TOPREAL9:16;
then
A48:Ball(Hp,r22) c= cl_Ball(Hp,r2) by A45;
then reconsider BI = Ball(Hp,r22) as Subset of Tball(0.TR,1)
by A43,XBOOLE_1:1;
BI c= hIU by A42,A47,A45;
then
A49: h"BI c= h"hIU by RELAT_1:143;
reconsider hBI=h"BI as Subset of M by A33,XBOOLE_1:1;
BI is open by TSEP_1:9;
then h"BI is open by A31,TOPGRP_1:26;
then
A50: hBI is open by A35,A49,TSEP_1:9;
|.Hp - Hp.|=0 by TOPRNS_1:28;
then h.p in BI by A39;
then p in h"BI by A37,A32,A33,A34,FUNCT_1:def 7;
then p in Int hCL by A48,RELAT_1:143,TOPS_1:22,A50;
then reconsider hCL as a_neighborhood of p by CONNSP_2:def 1;
A51: Tball(0.TR,1) |CL = Tdisk(Hp,r2) by A30,PRE_TOPC:7;
then reconsider hh=h| (h"CL) as Function of M|hCL ,Tdisk(Hp,r2)
by A44,JORDAN24:12,A46;
hh is being_homeomorphism by A31,A51,METRIZTS:2,A44,A46;
then
A52:M|hCL,Tdisk(Hp,r2) are_homeomorphic by T_0TOPSP:def 1;
Tdisk(Hp,r2),Tdisk(0.TR,1) are_homeomorphic by Lm1,A39;
hence thesis by A52,BORSUK_3:3,A39;
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 A26;
hence thesis by Def4;
end;
hence thesis;
end;
::$N Dimension of the Cartesian Product of Locally Euclidean Spaces
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;
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 Def3;
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 Def3;
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;
::$N Dimension of the Interior of Locally Euclidean Spaces
registration
let n;
let M be n-locally_euclidean non empty TopSpace;
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,Def7;
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) = 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,A11;
then
A12: Int hum = hum by TOPS_1:23;
A13: q in Int U by CONNSP_2:def 1;
then
A14: 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 A14,A9,FUNCT_1:def 6;
then consider s be Real such that
A15: s>0 and
A16: Ball(HQ,s) c= hum by A12,GOBOARD6:5;
A17: Ball(HQ,s)=Ball(hq,s) by TOPREAL9:13;
then reconsider BB=Ball(hq,s) as Subset of Tball(0.TR,1)
by A16,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 A16,A17,RELAT_1:143;
then
A18: 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 A18,XBOOLE_1:1,A1;
hBBM is open by TSEP_1:9,A18;
then
A19: HBB is open by TSEP_1:9;
|.hq-hq.|=0 by TOPRNS_1:28;
then hq in BB by A15;
then p in HBB by FUNCT_1:def 7,A13,A4,A9,A7;
then
A20: p in Int HBB by A19,TOPS_1:23;
A21: 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
A22: Tball(0.TR,1) | (h.:hBB) = TR|Ball(hq,s) by A11,PRE_TOPC:7;
reconsider HBB as a_neighborhood of p by A20,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 A3,A22,A23,A21,METRIZTS:2;
then
A24: MI|HBB,Tball(hq,s) are_homeomorphic by T_0TOPSP:def 1;
take HBB;
Tball(hq,s),Tball(0.TR,1) are_homeomorphic by A15,Th3;
hence thesis by A15,A24,BORSUK_3:3;
end;
hence thesis by Th13;
end;
end;
::$N Dimension of the Boundary of Locally Euclidean Spaces
registration
let n be non zero Nat;
let M be with_boundary n-locally_euclidean non empty TopSpace;
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 Def3;
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 Th7;
end;
n-'1 = n1 by XREAL_0:def 2;
hence thesis by A2,Th13;
end;
end;
begin :: Connected Components of Locally Euclidean Spaces
theorem Th14:
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 Def2;
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 A24: 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
A25: xp in R2 by A2,TARSKI:def 4;
A26: 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
A27: x in C;
then reconsider p=x as Point of M;
take I=Int (W.p);
A28: Int (W.p) c= W.p by TOPS_1:16;
W.p in rng W by A16,FUNCT_1:def 3;
then
A29: W.p is connected by A7;
A30: 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 A28,A27,XBOOLE_0:3;
then W.p c= C by A1,A29,CONNSP_3:16,A26;
hence I is open & I c= C & x in I by A30,CONNSP_2:def 1,A28;
end;
thus thesis;
end;
hence C is open by TOPS_1:25;
A31: R2 c= R1 by XBOOLE_1:36;
A32: 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
A33: x in y
and
A34: y in R2 by TARSKI:def 4;
y in R1 by A34,ZFMISC_1:56;
then y in IntW or y = C` by A21,ZFMISC_1:136;
then consider U be Subset of M such that
A35: y=Int U
and
A36: U in rng (W|C) by A34,ZFMISC_1:56;
A37: U is connected by A32,A36,A7;
A38: Int U c= U by TOPS_1:16;
consider p be object such that
A39: p in dom (W|C)
and
A40: (W|C).p = U by A36,FUNCT_1:def 3;
A41: W.p = U by A39,A40,FUNCT_1:47;
p in dom W by A39,RELAT_1:57;
then reconsider p as Point of M;
U is a_neighborhood of p by A4,A41;
then p in Int U by CONNSP_2:def 1;
then W.p meets C by A38,A39,A41,XBOOLE_0:3;
then U c= C by A41,A1,A37,CONNSP_3:16,A26;
hence thesis by A38,A33,A35;
end;
then
A42: union R2 = C by A24,TOPS_2:4;
A43:for x be object st x in R2 ex y be object st CC[x,y]
proof
let x be object;
assume
A44: x in R2;
then
A45: x <>C` by ZFMISC_1:56;
x in R1 by A44,ZFMISC_1:56;
then x in IntW by A21,A45,ZFMISC_1:136;
then consider U be Subset of M such that
A46: x=Int U
and
A47: U in rng (W|C);
consider y be object such that
A48: y in dom (W|C)
and
A49: (W|C).y = U by A47,FUNCT_1:def 3;
take y;
thus y in C by A48;
let A be Subset of M;
thus thesis by A48,FUNCT_1:47,A46,A49;
end;
consider cc be Function such that
A50: dom cc = R2 & for x be object st x in R2 holds CC[x,cc.x]
from CLASSES1:sch 1(A43);
CC[xp,cc.xp] by A25,A50;
then reconsider cp = cc.xp as Point of M;
consider n such that
A51: 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;
A52: Int (W.cp) = xp by A25,A50;
A53: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A54:P[k];
assume
A55: k+1 <= card R2;
then consider R3 be Subset-Family of M such that
A56: card R3 = k
and
A57: R3 c= R2
and
A58: union (W.:(cc.:R3)) is connected Subset of M
and
A59: 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,A54;
k < card R2 by A55,NAT_1:13;
then k in Segm (card R2) by NAT_1:44;
then R2\R3 <> {} by A56,CARD_1:68;
then consider r23 be object such that
A60: r23 in R2\R3 by XBOOLE_0:def 1;
reconsider r23 as set by TARSKI:1;
A61: r23 in R2 by A60,XBOOLE_0:def 5;
then
A62: r23 <> C` by ZFMISC_1:56;
r23 in R1 by A61,ZFMISC_1:56;
then r23 in IntW by A21,A62,ZFMISC_1:136;
then
A63:ex B be Subset of M st Int B = r23 & B in rng (W|C);
A64: r23 c= union (R2\R3) by A60,ZFMISC_1:74;
per cases;
suppose
k>0;
then R3 is non empty by A56;
then consider r3 be set such that
A65: r3 in R3;
A66: r3 <> C` by A57,A65,ZFMISC_1:56;
r3 in R1 by A57,A65,ZFMISC_1:56;
then r3 in IntW by A21,A66,ZFMISC_1:136;
then
A67: ex A be Subset of M st Int A = r3 & A in rng (W|C);
r3 c= union R3 by A65,ZFMISC_1:74;
then reconsider U3=union R3 as non empty Subset of M
by A32,A67,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
A68: D2 = U3 by XBOOLE_1:28, A42,A57,ZFMISC_1:77;
(R2\R3) \/R3 = R2\/R3 by XBOOLE_1:39
.= R2 by A57,XBOOLE_1:12;
then U3\/U23 = C by A42,ZFMISC_1:78;
then
A69: U3\/U23 =[#]MC by PRE_TOPC:def 5;
R3 c= R1 by A31,A57;
then R3 is open by A21,XBOOLE_1:1,A6,TOPS_2:11;
then
A70: D2 is open by TOPS_2:19,CONNSP_3:28;
A71: R2\R3 c= R2 by XBOOLE_1:36;
then R2\R3 c= R1 by A31;
then R2\R3 is open by A21,XBOOLE_1:1,A6,TOPS_2:11;
then
A72: D23 is open by TOPS_2:19,CONNSP_3:28;
D23 = U23 /\C by CONNSP_3:def 5;
then
A73: D23 =U23 by XBOOLE_1:28,A71,A42,ZFMISC_1:77;
U23<>{}MC by A64,A32,A63,A7;
then consider m be object such that
A74: m in U3
and
A75: m in U23 by A70,A72,A68,A73,A69,CONNSP_1:11,XBOOLE_0:3;
consider m1 be set such that
A76: m in m1
and
A77: m1 in R3 by A74,TARSKI:def 4;
CC[m1,cc.m1] by A57,A77,A50;
then reconsider c1=cc.m1 as Point of M;
consider m2 be set such that
A78: m in m2
and
A79: m2 in R2\R3 by A75,TARSKI:def 4;
A80: m2 in R2 by A79,XBOOLE_0:def 5;
then CC[m2,cc.m2] by A50;
then reconsider c2=cc.m2 as Point of M;
set R4 = R3\/{Int (W.c2)};
R3 is finite by A56;
then reconsider R4 as finite Subset-Family of M;
take R4;
A81: Int (W.c2) = m2 by A80,A50;
then not Int (W.c2) in R3 by A79,XBOOLE_0:def 5;
hence card R4 = k+1 by A56,A57,CARD_2:41;
A82: m2 in R2 by A79,XBOOLE_0:def 5;
then {m2} c= R2 by ZFMISC_1:31;
hence
A83: R4 c= R2 by A81,A57,XBOOLE_1:8;
A84: W.c2 in rng W by A16,FUNCT_1:def 3;
A85: Int (W.c1) = m1 by A57,A77,A50;
thus union (W.:(cc.:R4)) is connected Subset of M
proof
reconsider UWR3=union (W.:(cc.:R3)) as connected Subset of M by A58;
A86: Int (W.c2) c= W.c2 by TOPS_1:16;
c1 in cc.:R3 by A77, A57,A50,FUNCT_1:def 6;
then
A87: W.c1 in W.:(cc.:R3) by A16,FUNCT_1:def 6;
Int (W.c1) c= W.c1 by TOPS_1:16;
then
A88: m in UWR3 by A87,A85,A76,TARSKI:def 4;
UWR3 c= Cl UWR3 by PRE_TOPC:18;
then Cl UWR3 meets W.c2 by A86,A81,A78, A88,XBOOLE_0:3;
then
A89: not UWR3, (W.c2) are_separated by CONNSP_1:def 1;
cc.:R4 = (cc.:R3) \/ cc.:{m2} by A81,RELAT_1:120
.= (cc.:R3) \/ Im(cc,m2) by RELAT_1:def 16
.= (cc.:R3) \/ {cc.m2} by FUNCT_1:59,A82,A50;
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
A90: union (W.:(cc.:R4)) = UWR3 \/ union {W.c2} by ZFMISC_1:78
.= UWR3 \/ (W.c2) by ZFMISC_1:25;
W.c2 is connected by A84,A7;
hence thesis by A89,CONNSP_1:17,A90;
end;
let a,b be Subset of M such that
A91: a in R4
and
A92: b=W.(cc.a);
per cases by A91,ZFMISC_1:136;
suppose
a in R3;
hence thesis by A92,A59;
end;
suppose
a = Int (W.c2);
then Int b = Int (W.c2) by A80,A50,A92;
then
A93: m in Int b by A80,A50,A78;
CC[a,cc.a] by A91,A83,A50;
then reconsider ca=cc.a as Point of M;
A94: M| (W.c1),Tdisk(0.TOP-REAL n,1) are_homeomorphic by A77, A59;
P[ca,W.ca] by A4;
then consider mm be Nat such that
A95: M|b,Tdisk(0.TOP-REAL mm,1) are_homeomorphic by A92;
Int (W.c1) = m1 by A57,A77,A50;
then n=mm by A94,A76,A93,XBOOLE_0:3,A95, BROUWER3:14;
hence M| b,Tdisk(0.TOP-REAL n,1) are_homeomorphic by A95;
end;
end;
suppose
A96: k=0;
reconsider R3={Int (W.cp)} as Subset-Family of M;
take R3;
thus card R3 = k+1 by A96,CARD_1:30;
thus
A97: R3 c= R2 by A52,A25,ZFMISC_1:31;
cc.:R3 = Im(cc,xp) by A52,RELAT_1:def 16
.= {cp} by FUNCT_1:59,A25,A50;
then W.:(cc.:R3) = Im(W,cp) by RELAT_1:def 16
.={W.cp} by A16,FUNCT_1:59;
then
A98: 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 A98,A7;
let a,b be Subset of M such that
A99: a in R3
and
A100: b=W.(cc.a);
CC[a,cc.a] by A99,A97,A50;
then reconsider ca=cc.a as Point of M;
Int (W.cp) = xp by A25,A50;
hence M| b,Tdisk(0.TOP-REAL n,1) are_homeomorphic
by A51, TARSKI:def 1,A99,A100;
end;
end;
take n;
A101: 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(A101,A53);
then P[card R2];
then consider R3 be Subset-Family of M such that
A102: card R3 = card R2
and
A103: R3 c= R2
and
A104: 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;
A105:R2 = R3 by A102,A103,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;
A106: [#]MC=C by PRE_TOPC:def 5;
then consider y be set such that
A107: q in y
and
A108: y in R2 by A42,TARSKI:def 4;
CC[y,cc.y] by A50,A108;
then reconsider c = cc.y as Point of M;
reconsider Wc=W.c as Subset of M;
A109: 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
A110:Wc is connected by A7;
A111:Int Wc = y by A50,A108;
then Wc meets C by A109,A107, A106,XBOOLE_0:3;
then
A112: Wc c= C by A110,A1,CONNSP_3:16,A26;
then W.c/\C = W.c by XBOOLE_1:28;
then
A113: D = W.c by CONNSP_3:def 5;
(Int Wc)/\C = Int Wc by A112,A109,XBOOLE_1:1, XBOOLE_1:28;
then DI = Int Wc by CONNSP_3:def 5;
then q in Int D by CONNSP_3:28,A107,A111,A113,A109,TOPS_1:22;
then
A114: D is a_neighborhood of q by CONNSP_2:def 1;
M| (W.c) =(M|C) |D by A113,A106,PRE_TOPC:7;
hence thesis by A114, A104,A105,A108;
end;
hence thesis by Def3;
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 Th14;
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 Th14;
M | [#]M,M are_homeomorphic by Th1;
then M is n-locally_euclidean by Th11,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
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;
end;
end;
registration
let M1,M2 be topological_manifold;
cluster [:M1,M2:] -> second-countable Hausdorff;
coherence;
end;