p/.n }; A9: P1 c= the carrier of Tn proof let x be object; assume x in P1; then ex p be Point of Tn st p=x & 0>p/.n; hence thesis; end; P2 c= the carrier of Tn proof let x be object; assume x in P2; then ex p be Point of Tn st p=x & 0

0;
then p in P2 by A20;
hence thesis by A21,A18,XBOOLE_0:def 5;
end;
p in Sphere(0.Tn,1) by A19,XBOOLE_0:def 4;
then |.p.|=1 by TOPREAL9:12;
hence thesis by A22,A2;
end;
set S1=P1` /\ Sphere(0.Tn,1);
A23: S1 c= Sp
proof
let xx be object;
A24: P1`=[#]Tn\P1 by SUBSET_1:def 4;
assume
A25: xx in S1;
then reconsider p=xx as Point of Tn;
len p =n by CARD_1:def 7;
then dom p = Seg n by FINSEQ_1:def 3;
then
A26: p/.n =p.n by PARTFUN1:def 6, FINSEQ_1:3,A8;
A27: p in P1` by A25,XBOOLE_0:def 4;
A28: p.n >= 0
proof
assume p.n <0;
then p in P1 by A26;
hence thesis by A27,A24,XBOOLE_0:def 5;
end;
p in Sphere(0.Tn,1) by A25,XBOOLE_0:def 4;
then |.p.|=1 by TOPREAL9:12;
hence thesis by A28,A1;
end;
Sp c= S1
proof
let xx be object;
assume xx in Sp;
then consider p be Point of Tn such that
A29: xx=p
and
A30: p.n>=0
and
A31: |.p.|=1 by A1;
p-0.Tn=p by RLVECT_1:13;
then
A32: p in Sphere(0.Tn,1) by A31;
len p =n by CARD_1:def 7;
then
A33: dom p = Seg n by FINSEQ_1:def 3;
A34: not p in P1
proof
assume p in P1;
then ex q be Point of Tn st p=q & 0>q/.n;
hence thesis by A33,PARTFUN1:def 6, FINSEQ_1:3,A8,A30;
end;
P1` = [#]Tn\P1 by SUBSET_1:def 4;
then p in P1` by A34,XBOOLE_0:def 5;
hence thesis by A32,XBOOLE_0:def 4,A29;
end;
hence thesis by A10,A17,XBOOLE_0:def 10,A23;
end;
end;
theorem Th3:
for TM be metrizable TopSpace st TM is finite-ind second-countable
for F be closed Subset of TM st ind (F`) <= n
for f be continuous Function of TM|F,Tunit_circle(n+1)
ex g being continuous Function of TM,Tunit_circle(n+1) st g|F=f
proof
defpred P[Nat] means
for TM be metrizable TopSpace st TM is finite-ind second-countable
for F be closed Subset of TM st ind F` <= $1
for f be continuous Function of TM|F,Tunit_circle($1 +1)
ex g being Function of TM,Tunit_circle($1+1) st g is continuous & g|F=f;
let TM be metrizable TopSpace such that
A1: TM is finite-ind second-countable;
let F be closed Subset of TM such that
A2: ind (F`) <= n;
A3:for n st P[n] holds P[n+1]
proof
let n;
set n1=n+1,n2=n1+1;
assume
A4: P[n];
set Tn1=TOP-REAL n1,Tn2=TOP-REAL n2,U=Tunit_circle(n1+1);
let TM be metrizable TopSpace;
assume
A5: TM is finite-ind second-countable;
let F be closed Subset of TM such that
A6: ind F` <= n1;
let f be continuous Function of (TM | F),U;
A7: [#](TM|F) = F by PRE_TOPC:def 5;
A8: dom f = the carrier of (TM|F) by FUNCT_2:def 1;
A9: dom f = the carrier of (TM|F) by FUNCT_2:def 1;
A10: [#](TM|F) = F by PRE_TOPC:def 5;
per cases;
suppose
A11: F is empty;
take g=TM-->the Point of U;
g|F={} by A11;
hence thesis by A11;
end;
suppose
A12: F is non empty;
set Sn= {p where p is Point of Tn2: p.n2<=0 & |.p.|=1};
set Sp= {p where p is Point of Tn2: p.n2>=0 & |.p.|=1};
A13: Sp c= the carrier of Tn2
proof
let x be object;
assume x in Sp;
then ex p be Point of Tn2 st p=x & p.n2>=0 & |.p.|=1;
hence thesis;
end;
Sn c= the carrier of Tn2
proof
let x be object;
assume x in Sn;
then ex p be Point of Tn2 st p=x & p.n2<=0 & |.p.|=1;
hence thesis;
end;
then reconsider Sp,Sn as Subset of Tn2 by A13;
A14: Sn = {t where t is Point of Tn2: t.(n1+1)<=0 & |.t.|=1};
A15: Sp = {l where l is Point of Tn2: l.(n1+1)>=0 & |.l.|=1};
then reconsider s1=Sp,s2=Sn as closed Subset of Tn2 by A14,Th2;
A16: [#] (Tn2|s2) = s2 by PRE_TOPC:def 5;
U = Tcircle(0.Tn2,1) by TOPREALB:def 7;
then
A17: the carrier of U = Sphere(0.Tn2,1) by TOPREALB:9;
A18: s1 c= the carrier of U
proof
let x be object;
assume x in s1;
then consider p be Point of Tn2 such that
A19: x=p
and
p.(n1+1)>=0
and
A20: |.p.|=1;
p-0.Tn2 = p by RLVECT_1:13;
hence thesis by A20,A19,A17;
end;
A21: s2 c= the carrier of U
proof
let x be object;
assume x in s2;
then consider p be Point of Tn2 such that
A22: x=p
and
p.(n1+1)<=0
and
A23: |.p.|=1;
p-0.Tn2 = p by RLVECT_1:13;
hence thesis by A23,A22,A17;
end;
then reconsider S1=s1,S2=s2 as Subset of U by A18;
reconsider A1=f"S1,A2=f"S2 as Subset of TM by A7,XBOOLE_1:1;
A24: f.:(A1/\A2) c= (f.:A1) /\(f.:A2) by RELAT_1:121;
A25: f.:A2 c= s2 by FUNCT_1:75;
S1 is closed by TSEP_1:8;
then f"S1 is closed by PRE_TOPC:def 6;
then
A26: A1 is closed by A7,TSEP_1:8;
Sphere(0.Tn2,1) c= S1\/S2
proof
let x be object;
assume
A27: x in Sphere(0.Tn2,1);
then reconsider p=x as Point of Tn2;
A28: p.n2 >=0 or p.n2 <=0;
|.p.| = 1 by A27,TOPREAL9:12;
then p in Sp or p in Sn by A28;
hence thesis by XBOOLE_0:def 3;
end;
then rng f c= S1\/S2 by A17;
then
A29: f"rng f c= f"(S1\/S2) by RELAT_1:143;
f"rng f = dom f by RELAT_1:134;
then
A30: F = f"(S1\/S2) by A29,A7,FUNCT_2:def 1;
then
A31: F = A1\/A2 by RELAT_1:140;
then reconsider TFA12=A1/\A2 as Subset of TM|F by XBOOLE_1:29,A10;
A32: [#]((TM|F) |TFA12) =TFA12 by PRE_TOPC:def 5;
reconsider fa=f|TFA12 as Function of (TM|F) |TFA12,U| (f.:TFA12)
by A10,A12,JORDAN24:12;
A33: fa is continuous by JORDAN24:13, A10,A12;
dom f /\ TFA12 = TFA12 by A8,XBOOLE_1:28;
then
A34: dom fa=the carrier of ((TM|F) |TFA12) by A32, RELAT_1:61;
A35: (TM|F) | (f"S1) = TM|A1 by PRE_TOPC:7, A7;
then reconsider f1=f|A1 as Function of TM|A1,U| (f.:A1)
by A12,A7,JORDAN24:12;
A36: f1 is continuous by A35, A12,A10,JORDAN24:13;
A37: rng f1 c=the carrier of (U| (f.:A1));
A38: [#](U| (f.:A1))= f.:A1 by PRE_TOPC:def 5;
then
A39: rng f1 c= the carrier of U by XBOOLE_1:1;
A40: (TM|F) | (f"S2) = TM|A2 by PRE_TOPC:7, A7;
then reconsider f2=f|A2 as Function of TM|A2,U| (f.:A2)
by A12,A7,JORDAN24:12;
A41: f2 is continuous by A40, A12,A10,JORDAN24:13;
A42: [#](U| (f.:A2))= f.:A2 by PRE_TOPC:def 5;
then
A43: rng f2 c= the carrier of U by XBOOLE_1:1;
dom f1 = dom f/\A1 by RELAT_1:61;
then
A44: dom f1 = A1 by A9,XBOOLE_1:28;
[#](TM|A1) = A1 by PRE_TOPC:def 5;
then reconsider f1 as Function of TM|A1,U by A39,FUNCT_2:2,A44;
A45: rng f2 c=the carrier of (U| (f.:A2));
dom f2 = dom f/\A2 by RELAT_1:61;
then
A46: dom f2 = A2 by A9,XBOOLE_1:28;
[#](TM|A2) = A2 by PRE_TOPC:def 5;
then reconsider f2 as Function of TM|A2,U by A43,A46,FUNCT_2:2;
f.:A2 c= s2 by FUNCT_1:75;
then
A47: rng f2 c= s2 by A42,A45;
S2 is closed by TSEP_1:8;
then f"S2 is closed by PRE_TOPC:def 6;
then
A48: A2 is closed by A7,TSEP_1:8;
TM|F` is second-countable by A5;
then consider X1,X2 be closed Subset of TM such that
A49: [#]TM = X1\/X2
and
A50: A1 c=X1
and
A51: A2 c=X2
and
A52: A1/\X2=A1/\A2
and
A53: A1/\A2=X1/\A2
and
A54: ind((X1/\X2)\(A1/\A2))<=n1 qua ExtReal -1
by A31,TOPDIM_2:24,A5,A6,A26,A48;
set TX=TM| (X1/\X2);
A55: [#]TX = X1/\X2 by PRE_TOPC:def 5;
then reconsider TXA12=A1/\A2 as Subset of TX by A50,A51,XBOOLE_1:27;
(X1/\X2)\(A1/\A2)=TXA12` by A55,SUBSET_1:def 4;
then
A56: ind TXA12` <= n by A5,TOPDIM_1:21,A54;
set Un=Tunit_circle(n+1);
set TD=Tdisk(0.Tn1,1);
deffunc ff(Nat)=PROJ(n2,$1);
consider FF be FinSequence such that
A57: len FF = n1 & for k be Nat st k in dom FF holds FF.k=ff(k)
from FINSEQ_1:sch 2;
A58: rng FF c= Funcs(the carrier of Tn2,the carrier of R^1)
proof
let x be object;
assume x in rng FF;
then consider i be object such that
A59: i in dom FF
and
A60: FF.i = x by FUNCT_1:def 3;
reconsider i as Nat by A59;
ff(i) in Funcs(the carrier of Tn2,the carrier of R^1)
by FUNCT_2:8;
hence thesis by A57,A59,A60;
end;
A61: Ball(0.Tn1,1) c= Int cl_Ball(0.Tn1,1) by TOPREAL9:16,TOPS_1:24;
then
A62: cl_Ball(0.Tn1,1) is compact non boundary convex;
reconsider FF as FinSequence of
Funcs(the carrier of Tn2,the carrier of R^1) by A58,FINSEQ_1:def 4;
reconsider FF as Element of n1-tuples_on
Funcs(the carrier of Tn2,the carrier of R^1) by A57,FINSEQ_2:92;
set FFF=<:FF:>;
A63: s1/\s2 c= s2 by XBOOLE_1:17;
A64: FFF.:s2= cl_Ball(0.Tn1,1) by A57,Th1,A15;
then
A65: s2 is non empty;
A66: dom FFF=the carrier of Tn2 by FUNCT_2:def 1;
then s1/\dom FFF=s1 by XBOOLE_1:28;
then
A67: dom (FFF|s1)= s1 by RELAT_1:61;
s2/\dom FFF=s2 by XBOOLE_1:28,A66;
then
A68: dom (FFF|s2)= s2 by RELAT_1:61;
A69: the carrier of TD = cl_Ball(0.Tn1,1) by BROUWER:3;
then rng (FFF|s2) c= the carrier of TD by RELAT_1:115,A64;
then reconsider Fs2=FFF|s2 as Function of Tn2|s2,TD
by FUNCT_2:2,A16,A68;
A70: [#](Tn2|s1) = s1 by PRE_TOPC:def 5;
Fs2 is being_homeomorphism by A57,Th1,A15;
then
A71: s2,cl_Ball(0.Tn1,1) are_homeomorphic
by T_0TOPSP:def 1,METRIZTS:def 1;
A72: FFF.:s1= cl_Ball(0.Tn1,1) by A57,Th1,A14;
then
A73: s1 is non empty;
rng (FFF|s1) c= the carrier of TD by RELAT_1:115, A72,A69;
then reconsider Fs1=FFF|s1 as Function of Tn2|s1,TD
by A67,FUNCT_2:2,A70;
A74: Fs1.:(s1/\s2) c= FFF.:(s1/\s2) by RELAT_1:128;
A75: Fs1 is being_homeomorphism by A57,Th1,A14;
then
A76: rng Fs1 = [#]TD by TOPS_2:def 5;
f.:A1 c= s1 by FUNCT_1:75;
then WE: (f.:A1)/\(f.:A2) c= s1/\s2 by A25,XBOOLE_1:27;
then f.:(A1/\A2) c= s1/\s2 by A24;
then
A78: Fs1.:(f.:(A1/\A2)) c= Fs1.:(s1/\s2) by RELAT_1:123;
s1/\s2 c= s1 by XBOOLE_1:17;
then
A79: f.:(A1/\A2) c= s1 by WE,A24;
[#](U| (f.:TFA12))=f.:TFA12 by PRE_TOPC:def 5;
then
A80: rng fa c= the carrier of Tn2|s1 by A79,A70;
then reconsider fa as Function of (TM|F) |TFA12,U
by XBOOLE_1:1,A70,A34,FUNCT_2:2;
A81: fa is continuous by A33,PRE_TOPC:26;
rng fa c= the carrier of Tn2 by A17,XBOOLE_1:1;
then reconsider fa as Function of (TM|F) |TFA12,Tn2 by FUNCT_2:2,A34;
A82: fa is continuous by A81,PRE_TOPC:26;
A83: Fs1" is continuous by A75,TOPS_2:def 5;
A84: FFF.:(s1/\s2) = Sphere(0.Tn1,1) by A57,Th1;
then Fs1.:(s1/\s2) = Sphere(0.Tn1,1) by XBOOLE_1:17,RELAT_1:129;
then
A85: (Fs1").:Sphere(0.Tn1,1) = Fs1"(Fs1.:(s1/\s2)) by TOPS_2:55,A75,A76
.= s1/\s2 by FUNCT_1:94,A67,A75,XBOOLE_1:17;
set A2X=A2 \/ (X1/\X2);
set A1X=A1 \/ (X1/\X2);
A86: X2=[#](TM|X2) by PRE_TOPC:def 5;
(TM|F) |TFA12 = TM| (A1/\A2) by PRE_TOPC:7, A31,XBOOLE_1:29;
then
A87: (TM|F) |TFA12 = TX |TXA12 by PRE_TOPC:7,A50,A51,XBOOLE_1:27;
then reconsider fa as Function of TX |TXA12,Tn2|s1
by A34,FUNCT_2:2,A80;
reconsider Ffa=Fs1*fa as Function of TX|TXA12,TD by A73;
A88: [#](TX |TXA12) = TXA12 by PRE_TOPC:def 5;
then
A89: dom Ffa = A1/\A2 by FUNCT_2:def 1;
rng Ffa = Ffa.:dom Ffa by RELAT_1:113
.= (Fs1*fa).:(A1/\A2) by A88,FUNCT_2:def 1
.= Fs1.:(fa.:(A1/\A2)) by RELAT_1:126;
then E: rng Ffa c= Fs1.:(f.:(A1/\A2)) by RELAT_1:123, RELAT_1:128;
then
A90: rng Ffa c= Fs1.:(s1/\s2) by A78;
A91: rng Ffa c= Sphere(0.Tn1,1) by E,A78,A74,A84;
fa is continuous by A82,PRE_TOPC:27,A87;
then
A92: Ffa is continuous by TOPS_2:46, A75, A73;
reconsider Ffa as Function of TX |TXA12,Tn1
by A91,XBOOLE_1:1,FUNCT_2:2,A89,A88;
Un = Tcircle(0.Tn1,1) by TOPREALB:def 7;
then
A93: the carrier of Un = Sphere(0.Tn1,1) by TOPREALB:9;
then reconsider H=Ffa as Function of TX |TXA12,Un
by FUNCT_2:2,A89,A88,A90,A74,XBOOLE_1:1,A84;
Ffa is continuous by A92,PRE_TOPC:26;
then reconsider H as continuous Function of TX |TXA12,Un
by PRE_TOPC:27;
TXA12 is closed by A26,A48,TSEP_1:8;
then consider g be Function of TX, Un such that
A94: g is continuous
and
A95: g|TXA12 = H by A5,A56, A4;
A96: rng g c= the carrier of Tn1 by A93,XBOOLE_1:1;
A97: dom g=the carrier of TX by FUNCT_2:def 1;
A98: rng g c= the carrier of Un;
reconsider g as Function of TX, Tn1 by A97,A96,FUNCT_2:2;
A99: g is continuous by A94,PRE_TOPC:26;
the carrier of Un c= the carrier of TD by A93,A69,TOPREAL9:17;
then reconsider g as Function of TX,TD by A98,XBOOLE_1:1,FUNCT_2:2,A97;
reconsider G=(Fs1")*g as Function of TX,Tn2|s1;
A100: dom G = the carrier of TX by FUNCT_2:def 1,A73;
g is continuous by A99,PRE_TOPC:27;
then
A101: G is continuous by A83,TOPS_2:46;
A102: rng G c= s1 by A70;
then reconsider G as Function of TX,Tn2 by XBOOLE_1:1,FUNCT_2:2,A100;
A103: G is continuous by PRE_TOPC:26,A101;
reconsider G as Function of TX,U by A18,A102,XBOOLE_1:1,FUNCT_2:2,A100;
A104: G is continuous by PRE_TOPC:27,A103;
A105: rng fa c= dom Fs1 by A67,A70;
A106: G|TXA12 = (Fs1")*(g|TXA12) by RELAT_1:83
.= (Fs1"*Fs1)*fa by RELAT_1:36, A95
.= (id dom Fs1)*fa by TOPS_2:52, A75,A76
.= fa by RELAT_1:53,A105;
A107: now
let xx be object;
assume
A108: xx in dom f1/\dom G;
then
A109: xx in A1 by A44,XBOOLE_0:def 4;
xx in X2 by A108,A55,XBOOLE_0:def 4;
then
A110: xx in A1/\A2 by A109,A52,XBOOLE_0:def 4;
hence G.xx = (G|TXA12).xx by FUNCT_1:49
.= f.xx by A110,FUNCT_1:49,A106
.= f1.xx by A109,FUNCT_1:49;
end;
A111: now
let xx be object;
assume
A112: xx in dom f2/\dom G;
then
A113: xx in A2 by A46,XBOOLE_0:def 4;
xx in X1 by A112,A55,XBOOLE_0:def 4;
then
A114: xx in A1/\A2 by A113,A53,XBOOLE_0:def 4;
hence G.xx = (G|TXA12).xx by FUNCT_1:49
.= f.xx by A114,FUNCT_1:49, A106
.= f2.xx by A113,FUNCT_1:49;
end;
rng G = G.:dom G by RELAT_1:113
.= (Fs1").:(g.:dom G) by RELAT_1:126
.= (Fs1").:(rng g) by A97,A100,RELAT_1:113;
then rng G c= s1/\s2 by A85,A93,A98,RELAT_1:123;
then rng G c= s2 by A63;
then
A115: rng f2 \/rng G c= s2 by XBOOLE_1:8, A47;
f2 is continuous by A41,PRE_TOPC:26;
then reconsider f2G=f2+*G as continuous Function of TM|A2X,U
by A111,PARTFUN1:def 4,A104,A48,TOPGEN_5:10;
A116: dom f2G = the carrier of TM|A2X by FUNCT_2:def 1;
A117: rng f2G c= rng f2 \/rng G by FUNCT_4: 17;
then rng f2G c= s2 by A115;
then reconsider f2G as Function of TM|A2X,Tn2
by XBOOLE_1:1,FUNCT_2:2,A116;
A118: f2G is continuous by PRE_TOPC:26;
reconsider f2G as Function of TM|A2X,Tn2|s2
by FUNCT_2:2,A116,A115,A117,XBOOLE_1:1,A16;
cl_Ball(0.Tn1,1) is compact non boundary convex by A61;
then consider H2 being Function of TM,Tn2|s2 such that
A119: H2 is continuous
and
A120: H2|A2X=f2G by A118,PRE_TOPC:27,A71, TIETZE_2:24, A48;
A121: TM is non empty by A12;
then reconsider H2X=H2|X2 as Function of TM|X2,(Tn2|s2) | (H2.:X2)
by JORDAN24:12,A65;
A122: H2X is continuous by JORDAN24:13,A65,A121,A119;
dom H2 = the carrier of TM by FUNCT_2:def 1,A65;
then
A123: dom H2X = X2/\the carrier of TM by RELAT_1:61;
then
A124: dom H2X= the carrier of TM|X2 by XBOOLE_1:28,A86;
f1 is continuous by A36,PRE_TOPC:26;
then reconsider f1G=f1+*G as continuous Function of TM|A1X,U
by A107,PARTFUN1:def 4,A104,A26,TOPGEN_5:10;
A125: dom f1G = the carrier of TM|A1X by FUNCT_2:def 1;
f.:A1 c= s1 by FUNCT_1:75;
then rng f1 c= s1 by A38,A37;
then
A126: rng f1 \/rng G c= s1 by A102,XBOOLE_1:8;
A127: rng f1G c= rng f1 \/rng G by FUNCT_4:17;
then rng f1G c= s1 by A126;
then reconsider f1G as Function of TM|A1X,Tn2
by XBOOLE_1:1,FUNCT_2:2,A125;
A128: f1G is continuous by PRE_TOPC:26;
reconsider f1G as Function of TM|A1X,Tn2|s1
by FUNCT_2:2,A125, A126,A127,XBOOLE_1:1,A70;
s1,cl_Ball(0.Tn1,1) are_homeomorphic
by T_0TOPSP:def 1,A75,METRIZTS:def 1;
then consider H1 being Function of TM,Tn2|s1 such that
A129: H1 is continuous
and
A130: H1|A1X=f1G by A62,A26,A128,PRE_TOPC:27,TIETZE_2:24;
reconsider H1X=H1|X1 as Function of TM|X1,(Tn2|s1) | (H1.:X1)
by A121,JORDAN24:12,A73;
A131: H1X is continuous by JORDAN24:13,A73,A121,A129;
[#]((Tn2|s1) | (H1.:X1)) = (H1.:X1) by PRE_TOPC:def 5;
then
A132: rng H1X c= the carrier of Tn2|s1 by XBOOLE_1:1;
dom H1 = the carrier of TM by FUNCT_2:def 1,A73;
then
A133: dom H1X = X1/\the carrier of TM by RELAT_1:61;
then
A134: dom H1X= X1 by XBOOLE_1:28;
X1=[#](TM|X1) by PRE_TOPC:def 5;
then
A135: dom H1X= the carrier of TM|X1 by A133,XBOOLE_1:28;
then reconsider H1X as Function of TM|X1,Tn2|s1 by A132, FUNCT_2:2;
A136: H1X is continuous by A131,PRE_TOPC:26;
A137: rng H1X c= s1 by A70;
[#]((Tn2|s2) | (H2.:X2)) = (H2.:X2) by PRE_TOPC:def 5;
then rng H2X c= the carrier of Tn2|s2 by XBOOLE_1:1;
then reconsider H2X as Function of TM|X2,Tn2|s2 by A124, FUNCT_2:2;
A138: H2X is continuous by A122,PRE_TOPC:26;
reconsider H1X as Function of TM|X1,Tn2
by A137,XBOOLE_1:1,A135,FUNCT_2:2;
A139: rng H2X c= s2 by A16;
then reconsider H2X as Function of TM|X2,Tn2
by XBOOLE_1:1,A124,FUNCT_2:2;
A140: H2X is continuous by A138,PRE_TOPC:26;
A141: now
let xx be object;
assume
A142: xx in dom H1X/\dom H2X;
then
A143: H2X.xx=H2.xx by A86,FUNCT_1:49;
xx in X1 by A142,A134,XBOOLE_0:def 4;
then
A144: H1X.xx=H1.xx by FUNCT_1:49;
A145: xx in X1/\X2 by A142, A123,XBOOLE_1:28,A134;
then
A146: xx in A2X by XBOOLE_0:def 3;
xx in A1X by A145, XBOOLE_0:def 3;
then
A147: H1.xx = (H1|A1X).xx by FUNCT_1:49;
A148: f2G.xx=G.xx by A145,A100,A55,FUNCT_4:13;
f1G.xx = G.xx by A145,A100,A55,FUNCT_4:13;
hence H1X.xx = H2X.xx
by A148,A147,A146,FUNCT_1:49,A144,A143,A120,A130;
end;
H1X is continuous by A136,PRE_TOPC:26;
then reconsider H12=H1X+*H2X as continuous Function of
TM| (X1\/X2),Tn2 by A140,A141,PARTFUN1:def 4,TOPGEN_5:10;
A149: TM| (X1\/X2) = the TopStruct of TM by A49,TSEP_1:93;
then reconsider H12 as Function of TM,Tn2;
A150: rng H12 c= rng H1X \/ rng H2X by FUNCT_4:17;
F/\X1 = (A1\/A2)/\X1 by A30,RELAT_1:140
.= (A1/\X1)\/(A2/\X1) by XBOOLE_1:23
.= A1 \/(A2/\X1) by A50,XBOOLE_1:28
.= A1 by A53,XBOOLE_1:17,XBOOLE_1:12;
then
A151: H1X|F= H1|A1 by RELAT_1:71;
f1G=G+*f1 by A107,PARTFUN1:def 4,FUNCT_4:34;
then
A152: f1G|A1 =f1 by FUNCT_4:23, A44;
A153: F/\X2 = (A1\/A2)/\X2 by A30,RELAT_1:140
.= (A1/\X2)\/(A2/\X2) by XBOOLE_1:23
.= (A1/\X2)\/A2 by A51,XBOOLE_1:28
.= A2 by A52,XBOOLE_1:17,XBOOLE_1:12;
A154: H2|A2 = f2G|A2 by A120,RELAT_1:74, XBOOLE_1:7;
rng H1X \/ rng H2X c= s1\/s2 by A139,A137,XBOOLE_1:13;
then
A155: rng H12 c= s1\/s2 by A150;
A156: dom H12 = the carrier of TM by FUNCT_2:def 1;
A157: H12 is continuous by PRE_TOPC:32,A149;
s1\/s2 c= Sphere(0.Tn2,1) by A18, A21,A17,XBOOLE_1:8;
then reconsider H12 as Function of TM,U
by A155,XBOOLE_1:1,A17,A156,FUNCT_2:2;
take H12;
thus H12 is continuous by PRE_TOPC:27,A157;
A158: H1|A1 = f1G|A1 by A130,XBOOLE_1:7,RELAT_1:74;
f2G=G+*f2 by A111,PARTFUN1:def 4,FUNCT_4:34;
then
A159: f2G|A2 =f2 by FUNCT_4:23,A46;
thus H12|F = H1X|F +*H2X|F by FUNCT_4:71
.= f1+*f2 by A152,A159,A158,A154,A151, RELAT_1:71,A153
.= f| (A1\/A2) by FUNCT_4:78
.= f by A31,A10;
end;
end;
let f be continuous Function of TM|F,Tunit_circle(n+1);
A160:P[0 qua Nat]
proof
reconsider Z=0 as Real;
set TR=TOP-REAL 1,U=Tunit_circle(0+1);
let TM be metrizable TopSpace;
assume
A161: TM is finite-ind second-countable;
let F be closed Subset of TM;
assume
A162: ind F` <= 0;
let f be continuous Function of TM|F,U;
A164: f"rng f = f"(the carrier of U) by RELAT_1:143,135;
U = Tcircle(0.TR,1) by TOPREALB:def 7;
then
A165: the carrier of U = Sphere(0.TR,1) by TOPREALB:9;
0.TR = 0*(0+1) by EUCLID:70
.= <*0 *> by FINSEQ_2:59;
then
A166: {<* Z qua ExtReal-1 *>,<* Z qua ExtReal+1 *>} =Fr Ball(0.TR,1)
by TOPDIM_2:18;
A167: Fr Ball(0.TR,1)= Sphere(0.TR,1) by JORDAN:24;
then reconsider mONE = <*-1*>,ONE=<*1*> as Point of U
by A165,TARSKI:def 2,A166;
reconsider Q={ONE},Q1={mONE} as closed Subset of U;
set F1=f"Q,F2=f"Q1;
A168: [#](TM|F)=F by PRE_TOPC:def 5;
then reconsider A1=F1,A2=F2 as Subset of TM by XBOOLE_1:1;
A169: dom f = F by A168,FUNCT_2:def 1;
Q\/Q1 = the carrier of U by A166,A167,A165,ENUMSET1:1;
then
A170: F1\/F2 = f"(the carrier of U) by RELAT_1:140
.= F by A164,RELAT_1:134,A169;
F2 is closed by PRE_TOPC:def 6;
then
A171: A2 is closed by TSEP_1:8,A168;
F1 is closed by PRE_TOPC:def 6;
then
A172: A1 is closed by TSEP_1:8,A168;
ONE<>mONE
proof
assume ONE=mONE;
then <*1*>.1 = -1 by FINSEQ_1:40;
hence thesis;
end;
then W: F1 misses F2 by ZFMISC_1:11,FUNCT_1:71;
TM|F` is second-countable by A161;
then consider X1,X2 be closed Subset of TM such that
A174: [#]TM = X1\/X2
and
A175: A1 c=X1
and
A176: A2 c=X2
and A1/\X2=A1/\A2 & A1/\A2=X1/\A2
and
A177: ind((X1/\X2)\(A1/\A2))<=0 qua ExtReal-1
by A161,A162,A170,TOPDIM_2:24,A172,A171;
ind (X1/\X2) >= -1 by TOPDIM_1:5,A161;
then
A178: X1/\X2 is empty by A177,W,XXREAL_0:1,TOPDIM_1:6,A161;
set h1=(TM|X1)-->ONE,h2=(TM|X2)-->mONE;
A179: [#](TM|X1)=X1 by PRE_TOPC:def 5;
A180: dom h2 = the carrier of (TM|X2) by FUNCOP_1:13;
A181: [#](TM|X2)=X2 by PRE_TOPC:def 5;
dom h1 = the carrier of (TM|X1) by FUNCOP_1:13;
then h1 tolerates h2
by A178,A179,A180,A181,XBOOLE_0:def 7,PARTFUN1:56;
then reconsider h12=h1+*h2 as continuous Function of TM| ([#]TM),U
by A174, TOPGEN_5:10;
[#] (TM| ([#]TM)) = [#]TM by PRE_TOPC:def 5;
then reconsider H12=h12 as Function of TM,U;
A182: for x be object st x in F holds (H12|F).x = f.x
proof
let x be object;
assume
A183: x in F;
then
A184: (H12|F).x=h12.x by FUNCT_1:49;
per cases by A183,A170,XBOOLE_0:def 3;
suppose
A185: x in F1;
then not x in dom h2 by A175,A178,XBOOLE_0:def 4,A181;
then
A186: H12.x=h1.x by FUNCT_4:11;
A187: f.x in {ONE} by A185,FUNCT_1:def 7;
h1.x = ONE by A185,A175,A179,FUNCOP_1:7;
hence thesis by A187,TARSKI:def 1,A186,A184;
end;
suppose
A188: x in F2;
then
A189: f.x in {mONE} by FUNCT_1:def 7;
A190: h2.x = mONE by A188,A176,A181,FUNCOP_1:7;
H12.x=h2.x by A188,A176,A180,A181,FUNCT_4:13;
hence thesis by A189,TARSKI:def 1,A190,A184;
end;
end;
take H12;
TM| ([#]TM) = the TopStruct of TM by TSEP_1:93;
hence H12 is continuous by PRE_TOPC:32;
dom H12 = the carrier of TM by FUNCT_2:def 1;
then dom (H12|F)=F by RELAT_1:62;
hence thesis by A182,A168,FUNCT_2:def 1;
end;
for n holds P[n] from NAT_1:sch 2(A160,A3);
then ex g be Function of TM, Tunit_circle(n+1) st
g is continuous & g|F=f by A1,A2;
hence thesis;
end;
theorem Th4:
not p in A & r>0 implies
ex h be Function of (TOP-REAL n) |A,(TOP-REAL n) |Sphere(p,r) st
h is continuous & h|Sphere(p,r) = id (A/\Sphere(p,r))
proof
set TR=TOP-REAL n;
assume that
A1: not p in A
and
A2: r>0;
set S=Sphere(p,r);
per cases;
suppose
A3: A is empty;
set h = the continuous Function of TR|A,TR;
reconsider H=h as Function of TR|A,TR|S by A3;
take H;
thus thesis by A3,PRE_TOPC:27;
end;
suppose
A4: A is non empty;
A<>{p} by A1,TARSKI:def 1;
then
A5: A\{p} <>{} by A4,ZFMISC_1:58;
set TRS=TR|S;
set nN=n NormF,t=transl(-p,TR),P=transl(p,TR);
A6: A\{p} c= (the carrier of TR)\{p} by XBOOLE_1:33;
(the carrier of TR)\{p}={p}` by SUBSET_1:def 4;
then reconsider cTRp=(the carrier of TR)\{p} as
non empty open Subset of TR by A5,A6;
set TRp=TR|cTRp,tt=t|TRp;
A7: [#]TRp = cTRp by PRE_TOPC:def 5;
then reconsider AA=A as Subset of TRp by A1,ZFMISC_1:57,A6;
reconsider Ir=tt[#]r as Function of TRp,TR by TOPREALC:37;
reconsider IrNt=Ir(nN*tt) as Function of TRp,TR by TOPREALC:46;
A8: tt = t|the carrier of TRp by TMAP_1:def 4;
not 0 in rng(nN*tt)
proof
assume 0 in rng(nN*tt);
then consider x be object such that
A9: x in dom (nN*tt)
and
A10: (nN*tt).x=0 by FUNCT_1:def 3;
tt.x in dom nN by A9,FUNCT_1:11;
then reconsider Tx=tt.x as Point of TR;
reconsider Tx as Element of REAL n by EUCLID:22;
A11: x in dom tt by A9,FUNCT_1:11;
then
A12: t.x=tt.x by A8,FUNCT_1:47;
x in dom t by A11,A8,RELAT_1:57;
then reconsider X=x as Point of TR;
0 = nN.Tx by A9,FUNCT_1:12,A10
.= |.Tx.| by JGRAPH_4:def 1;
then 0*n=Tx by EUCLID:8;
then 0.TR = Tx by EUCLID:70
.= -p+X by A12,RLTOPSP1:def 10;
then X = --p by RLVECT_1:def 10
.=p;
then x in {p} by TARSKI:def 1;
hence contradiction by A9,A7,XBOOLE_0:def 5;
end;
then nN*tt is non-empty by RELAT_1:def 9;
then reconsider IrNt as continuous Function of TRp,TR;
set h=(P*IrNt) | (TRp|AA);
A13: h= (P*IrNt) | the carrier of (TRp|AA) by TMAP_1:def 4;
reconsider h as continuous Function of (TRp|AA),TR by A4;
(TRp|AA) = TR|A by PRE_TOPC:7, A7;
then reconsider h as continuous Function of (TR|A),TR;
A14: [#](TR|A)=A by PRE_TOPC:def 5;
then
A15: dom h = A by FUNCT_2:def 1;
A16: dom tt = cTRp by A7,FUNCT_2:def 1;
A17: rng h c= S
proof
let y be object;
assume y in rng h;
then consider x be object such that
A18: x in dom h
and
A19: h.x=y by FUNCT_1:def 3;
reconsider x as Point of TR by A18,A15;
tt.x=t.x by A7,A18,A15,FUNCT_1:47,A8,A16;
then
A20: tt.x = -p+x by RLTOPSP1:def 10;
dom (nN*tt) = cTRp by A7,FUNCT_2:def 1;
then (nN*tt).x = nN.(tt.x) by A7,A18,A15,FUNCT_1:12;
then
A21: (nN*tt).x = |.-p+x.| by A20,JGRAPH_4:def 1;
A22: x in dom (P*IrNt) by A13,A18,RELAT_1:57;
then x in dom IrNt by FUNCT_1:11;
then
A23: IrNt.x = Ir.x (/) (nN*tt).x by VALUED_2:72;
dom Ir = cTRp by A7,FUNCT_2:def 1;
then Ir.x = r*(-p+x) by A20, A7,A18,A15,VALUED_2:def 39;
then
A24: IrNt.x = (1 / |.-p+x.|)*(r*(-p+x)) by A21,A23,VALUED_2:def 32;
then reconsider Fx=IrNt.x as Point of TR;
h.x = (P*IrNt).x by A13,A18,FUNCT_1:47;
then
A25: h.x = P.Fx by A22,FUNCT_1:12
.= p+Fx by RLTOPSP1:def 10;
--p=p;
then -p+x<>0.TR by A18,A1,A15,RLVECT_1:6;
then
A26: -p+x<>0*n by EUCLID:70;
A27: -p+x is Element of REAL n by EUCLID:22;
A28: p+Fx-p = Fx+(p+-p) by RLVECT_1:def 3
.= Fx+0.TR by RLVECT_1:def 10
.= Fx by RLVECT_1:def 4;
|.Fx.| = |.((1 / |.-p+x.|)*r)*(-p+x).| by A24,RLVECT_1:def 7
.= |. (1 / |.-p+x.|)*r .|* |.-p+x.| by EUCLID:11
.= |. 1 / |.-p+x.| .|* |.r.|* |.-p+x.| by COMPLEX1:65
.= |.1 / |.-p+x.|.|*r*|.-p+x.| by ABSVALUE:def 1,A2
.= |.1 / |.-p+x.|.|*r*|.|.-p+x.|.| by ABSVALUE:def 1
.= |.1 / |.-p+x.|.|*|.|.-p+x.|.|*r
.= 1*r by ABSVALUE:6, A26,EUCLID:8,A27
.=r;
hence thesis by A28,A25,A19;
end;
[#]TRS = S by PRE_TOPC:def 5;
then reconsider h as Function of TR|A,TR|S by A17,A14,A15,FUNCT_2:2;
A29: dom (h|S) = A/\S by A15,RELAT_1:61;
A31: for x be object st x in dom (h|S) holds (h|S).x = id(A/\S).x
proof
let y be object;
assume
A32: y in dom (h|S);
then reconsider x=y as Point of TR by A29;
A33: x in dom h by A32,RELAT_1:57;
then
A34: h.x = (P*IrNt).x by A13,FUNCT_1:47;
tt.x=t.x by A7,A33,A15,FUNCT_1:47,A8,A16;
then
A35: tt.x = -p+x by RLTOPSP1:def 10;
x-p = -p+x;
then
A36: |.-p+x.| =r by A32,TOPREAL9:9;
A37: x in dom (P*IrNt) by A13,A33,RELAT_1:57;
then x in dom IrNt by FUNCT_1:11;
then
A38: IrNt.x = Ir.x (/) (nN*tt).x by VALUED_2:72;
dom (nN*tt) = cTRp by A7, FUNCT_2:def 1;
then (nN*tt).x = nN.(tt.x) by A7,A33,A15,FUNCT_1:12;
then
A39: (nN*tt).x = |.-p+x.| by A35,JGRAPH_4:def 1;
dom Ir = cTRp by A7,FUNCT_2:def 1;
then Ir.x = r*(-p+x) by A35, A7,A33,A15,VALUED_2:def 39;
then
A40: IrNt.x = (1 / |.-p+x.|)*(r*(-p+x)) by A39,A38,VALUED_2:def 32
.= (1/r *r) *(-p+x) by A36,RLVECT_1:def 7
.= 1*(-p+x) by XCMPLX_1:87,A2
.= -p+x by RLVECT_1:def 8;
thus (h|S).y=h.x by A32,FUNCT_1:47
.=P.(-p+x) by A34, A37,FUNCT_1:12,A40
.= p+(-p+x) by RLTOPSP1:def 10
.= (p+-p)+x by RLVECT_1:def 3
.= 0.TR+x by RLVECT_1:def 10
.= x by RLVECT_1:def 4
.= id(A/\S).y by A32,A29,FUNCT_1:17;
end;
take h;
thus thesis by A31,A15,PRE_TOPC:27,RELAT_1:61;
end;
end;
theorem Th5:
r + |.p-q.| <= s implies Ball(p,r) c= Ball(q,s)
proof
assume
A1: r+|.p-q.| <= s;
let x be object;
assume
A2: x in Ball(p,r);
then reconsider x as Point of TOP-REAL n;
|.x-p.|+|.p-q.| < r+|.p-q.| by A2,TOPREAL9:7,XREAL_1:6;
then
A3: |.x-p.|+|.p-q.| < s by A1,XXREAL_0:2;
A4: x is Element of REAL n by EUCLID:22;
A5:p is Element of REAL n by EUCLID:22;
q is Element of REAL n by EUCLID:22;
then |.x-q.| <= |.x-p.| + |.p-q.| by A4,A5,EUCLID:19;
then |.x-q.| < s by A3,XXREAL_0:2;
hence thesis;
end;
theorem Th6:
A is non boundary implies ind A = n
proof
set TR=TOP-REAL n;
set E=the empty Subset of TR;
consider Ia be affinely-independent Subset of TR such that
E c= Ia & Ia c= [#]TR
and
A1: Affin Ia = Affin [#]TR by RLAFFIN1:60;
A2: the TopStruct of TR=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider IA=Ia as finite Subset of Euclid n by TOPMETR:12;
IA <> {} by A1;
then consider X be object such that
A3: X in IA by XBOOLE_0:def 1;
reconsider X as Point of Euclid n by A3;
reconsider x=X as Point of TR by A2, TOPMETR:12;
A4: dim TR = n by RLAFFIN3:4;
[#]TR c= Affin [#]TR by RLAFFIN1:49;
then card Ia = (dim TR)+1 by A1,XBOOLE_0:def 10,RLAFFIN3:6;
then
A5: ind conv Ia = n by A4,SIMPLEX2:25;
set d=diameter IA;
A6: ind TR = n by SIMPLEX2:26;
Ia c= conv Ia by RLAFFIN1:2;
then
A7: conv Ia c= cl_Ball(X,d) by A3,SIMPLEX2:13;
assume A is non boundary;
then Int A <> {} by TOPS_1:48;
then consider y be object such that
A8: y in Int A by XBOOLE_0:def 1;
reconsider y as Point of TR by A8;
reconsider Y=y as Point of Euclid n by A2, TOPMETR:12;
consider r be Real such that
A9: r>0
and
A10: Ball(Y,r) c= A by A8,GOBOARD6:5;
set r2=r/2;
A11: n in NAT by ORDINAL1:def 12;
A12: Ball(Y,r)=Ball(y,r) by TOPREAL9:13;
d+0 < d+1 by XREAL_1:6;
then
A13: cl_Ball(x,d) c= Ball(x,d+1) by A11,JORDAN:21;
cl_Ball(X,d)=cl_Ball(x,d) by TOPREAL9:14;
then conv Ia c= Ball(x,d+1) by A13,A7;
then
A14: n <= ind Ball(x,d+1) by A5,TOPDIM_1:19;
d>=0 by TBSP_1:21;
then
A15: cl_Ball(x,d+1) is compact non boundary by Lm2;
cl_Ball(y,r2) c= Ball(y,r) by A9,XREAL_1:216,A11,JORDAN:21;
then cl_Ball(y,r2) c= A by A10,A12;
then
A16:ind cl_Ball(y,r2) <= ind A by TOPDIM_1:19;
cl_Ball(y,r2) is compact non boundary by A9, Lm2;
then ex h be Function of TR |cl_Ball(x,d+1),TR |cl_Ball(y,r2) st
h is being_homeomorphism & h.:Fr cl_Ball(x,d+1) = Fr cl_Ball(y,r2)
by A15,BROUWER2:7;
then cl_Ball(x,d+1),cl_Ball(y,r2) are_homeomorphic
by T_0TOPSP:def 1,METRIZTS:def 1;
then
A17:ind cl_Ball(x,d+1)=ind cl_Ball(y,r2) by TOPDIM_1:27;
Ball(x,d+1) c= cl_Ball(x,d+1) by TOPREAL9:16;
then ind Ball(x,d+1) <= ind cl_Ball(x,d+1) by TOPDIM_1:19;
then n <= ind cl_Ball(y,r2) by A17,A14, XXREAL_0:2;
then
A18: n<= ind A by A16,XXREAL_0:2;
ind A <= ind TR by TOPDIM_1:20;
hence thesis by A6,XXREAL_0:1,A18;
end;
::$N The Small Inductive Dimension of the Sphere
theorem Th7:
r>0 implies ind Sphere(p,r) = n-1
proof
set TR=TOP-REAL n;
A1: ind A <= i & ind B <=i & A is closed implies ind (A\/B)<=i
proof
set TT=the TopStruct of TR;
assume that
A2: ind A <= i
and
A3: ind B <=i
and
A4: A is closed;
reconsider a=A, b=B, AB=A\/B as Subset of TT;
A5: a is closed by A4,PRE_TOPC:31;
A6: TT|AB is second-countable;
A7: TT = TopSpaceMetr Euclid n by EUCLID:def 8;
A8: TT = TR| [#]TR by TSEP_1:93;
then
A9: ind b<=i by TOPDIM_1:22,A3;
ind a<= i by A8,TOPDIM_1:22,A2;
then ind AB <= i by A9,A5,A8, A7,A6,TOPDIM_2:5;
hence thesis by TOPDIM_1:22,A8;
end;
assume
A10: r>0;
per cases by NAT_1:25;
suppose
A11: n=0;
then
A12: p=0.TR by EUCLID:77;
Sphere(p,r)={}
proof
assume Sphere(p,r) <>{};
then consider x be object such that
A13: x in Sphere(p,r) by XBOOLE_0:def 1;
reconsider x as Point of TR by A13;
x = 0.TR by A11,EUCLID:77
.= 0*n by EUCLID:66;
then |.x.| = 0 by EUCLID:7;
hence contradiction by A12,A13,TOPREAL9:12,A10;
end;
hence thesis by TOPDIM_1:6,A11;
end;
suppose
A15: n=1;
then consider u be Real such that
A16: p=<*u*> by JORDAN2B:20;
set u1=|[u-r]|,u2=|[u+r]|;
card {u2}=1 by CARD_1:30;
then
A17: ind {u2} = 0 by TOPDIM_1:8, NAT_1:14;
card {u1}=1 by CARD_1:30;
then ind {u1}=0 by TOPDIM_1:8, NAT_1:14;
then
A18: ind ({u1}\/{u2}) = 0 by A17,A15,A1;
{<*u qua ExtReal-r*>,<*u qua ExtReal+r*>} = Fr Ball(p,r)
by A15,TOPDIM_2:18,A16,A10
.= Sphere(p,r) by A15,A10,JORDAN:24;
hence thesis by A18,ENUMSET1:1,A15;
end;
suppose
A19: n>1;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
reconsider n1 as non zero Element of NAT by A19;
set n2=n1+1;
set Tn1=TOP-REAL n1,Tn2=TOP-REAL n2,S=Sphere(0.Tn2,1);
set Sp = {s where s is Point of Tn2: s.n2>=0 & |.s.|=1},
Sn = {t where t is Point of Tn2: t.n2<=0 & |.t.|=1};
A20: Sp c= S
proof
let x be object;
assume x in Sp;
then consider s be Point of Tn2 such that
A21: x=s
and
s.n2>=0
and
A22: |.s.|=1;
s-0.Tn2 = s by RLVECT_1:13;
hence thesis by A22,A21;
end;
A23: [#](TR |cl_Ball(p,r)) = cl_Ball(p,r) by PRE_TOPC:def 5;
reconsider Spr=Sphere(p,r) as Subset of TR |cl_Ball(p,r)
by A23,TOPREAL9:17;
A24: cl_Ball(0.Tn2,1) is compact non boundary by Lm2;
cl_Ball(p,r) is compact non boundary by Lm2, A10;
then consider h be Function of TR | cl_Ball(p,r), Tn2 |cl_Ball(0.Tn2,1)
such that
A25: h is being_homeomorphism
and
A26: h.:Fr cl_Ball(p,r) = Fr cl_Ball(0.Tn2,1) by A24,BROUWER2:7;
A27: ind Spr = ind (h.:Spr) by A25,METRIZTS:3,TOPDIM_1:27;
A28: Sn c= S
proof
let x be object;
assume x in Sn;
then consider s be Point of Tn2 such that
A29: x=s
and
s.n2<=0
and
A30: |.s.|=1;
s-0.Tn2 = s by RLVECT_1:13;
hence thesis by A30,A29;
end;
then reconsider Sp,Sn as Subset of TOP-REAL n2 by A20,XBOOLE_1:1;
A31: S c= Sp\/Sn
proof
let x be object;
assume
A32: x in S;
then reconsider x as Point of Tn2;
A33: x.n2 >=0 or x.n2<=0;
|.x.|=1 by A32,TOPREAL9:12;
then x in Sp or x in Sn by A33;
hence thesis by XBOOLE_0:def 3;
end;
A34: Sn= {t where t is Point of TOP-REAL n2: t.n2<=0 & |.t.|=1};
then
A35: Sp is closed by Th2;
A36: Sp = {s where s is Point of TOP-REAL n2: s.n2>=0 & |.s.|=1};
A37: Sp,cl_Ball(0.Tn1,1) are_homeomorphic &
Sn,cl_Ball(0.Tn1,1) are_homeomorphic
proof
set TD=Tdisk(0.Tn1,1);
deffunc ff(Nat)=PROJ(n2,$1);
consider FF be FinSequence such that
A38: len FF = n1 & for k be Nat st k in dom FF holds FF.k=ff(k)
from FINSEQ_1:sch 2;
rng FF c= Funcs(the carrier of Tn2,the carrier of R^1)
proof
let x be object;
assume x in rng FF;
then consider i be object such that
A39: i in dom FF
and
A40: FF.i = x by FUNCT_1:def 3;
reconsider i as Nat by A39;
ff(i) in Funcs(the carrier of Tn2,the carrier of R^1) by FUNCT_2:8;
hence thesis by A38,A39,A40;
end;
then reconsider FF as FinSequence of
Funcs(the carrier of Tn2,the carrier of R^1) by FINSEQ_1:def 4;
reconsider FF as Element of n1-tuples_on
Funcs(the carrier of Tn2,the carrier of R^1) by A38,FINSEQ_2:92;
set FFF=<:FF:>;
A41: [#]TD = cl_Ball(0.Tn1,1) by PRE_TOPC:def 5;
FFF.:Sp= cl_Ball(0.Tn1,1) by A38,Th1,A34;
then
A42: rng (FFF|Sp) c= the carrier of TD by RELAT_1:115,A41;
A43: dom FFF=the carrier of Tn2 by FUNCT_2:def 1;
then Sn/\dom FFF=Sn by XBOOLE_1:28;
then
A44: dom (FFF|Sn)= Sn by RELAT_1:61;
Sp/\dom FFF=Sp by A43,XBOOLE_1:28;
then
A45: dom (FFF|Sp)= Sp by RELAT_1:61;
[#](Tn2|Sp) = Sp by PRE_TOPC:def 5;
then
reconsider Fsp=FFF|Sp as Function of Tn2|Sp,TD by A42,A45,FUNCT_2:2;
A46: [#] (Tn2|Sn) = Sn by PRE_TOPC:def 5;
FFF.:Sn= cl_Ball(0.Tn1,1) by A38,Th1,A36;
then rng (FFF|Sn) c= the carrier of TD by RELAT_1:115, A41;
then reconsider Fsn=FFF|Sn as Function of Tn2|Sn,TD by A46,FUNCT_2:2,A44;
A47: Fsn is being_homeomorphism by A38,Th1,A36;
Fsp is being_homeomorphism by A38,Th1,A34;
hence thesis by A47,T_0TOPSP:def 1,METRIZTS:def 1;
end;
A48: ind cl_Ball(0.Tn1,1) = n1 by Lm2,Th6;
then
A49: ind Sp=n1 by A37,TOPDIM_1:27;
Sp c= Sp\/Sn by XBOOLE_1:7;
then
A50: n1 <= ind (Sp\/Sn) by A49, TOPDIM_1:19;
ind Sn=n1 by A37,A48,TOPDIM_1:27;
then ind (Sp\/Sn) <= n1 by A35,A49,A1;
then
A51: ind (Sp\/Sn) = n1 by A50,XXREAL_0:1;
Fr cl_Ball(p,r) = Sphere(p,r) by BROUWER2:5,A10;
then h.:Spr = S by A26, BROUWER2:5;
then
A52: ind (h.:Spr) = ind S by TOPDIM_1:21;
Sp\/Sn c= S by A20,A28,XBOOLE_1:8;
then ind S= n1 by A31,XBOOLE_0:def 10,A51;
hence thesis by TOPDIM_1:21,A52,A27;
end;
end;
begin :: A Characterization of Open Sets in Euclidean Space
:: in Terms of Continuous Transformations
theorem Th8:
for p st n>0 & p in A & for r st r>0
ex U be open Subset of (TOP-REAL n) |A st
p in U & U c= Ball(p,r) &
for f be Function of (TOP-REAL n) | (A\U),Tunit_circle(n) st
f is continuous
ex h be Function of (TOP-REAL n) |A,Tunit_circle(n) st
h is continuous & h| (A\U) = f
holds p in Fr A
proof
let p;
set TRn=TOP-REAL n,cTRn=the carrier of TRn;
set CL=cl_Ball(0.TRn,1),S=Sphere(0.TRn,1);
set TS=Tunit_circle(n);
assume
A1: n > 0;
cTRn\{0.TRn}={0.TRn}` by SUBSET_1:def 4;
then reconsider cTR0=cTRn\{0.TRn} as non empty open Subset of TRn by A1;
set nN=n NormF;
set TRn0=TRn|cTR0;
A2: Int A c= A by TOPS_1:16;
set G= transl(p,TRn);
reconsider I=incl TRn0 as continuous Function of TRn0,TRn by TMAP_1:87;
A3: [#]TRn0=cTR0 by PRE_TOPC:def 5;
A4: nN|TRn0=nN|the carrier of TRn0 by TMAP_1:def 4;
not 0 in rng(nN|TRn0)
proof
assume 0 in rng(nN|TRn0);
then consider x be object such that
A5: x in dom(nN|TRn0)
and
A6: (nN|TRn0).x=0 by FUNCT_1:def 3;
x in dom nN by A4,A5,RELAT_1:57;
then reconsider x as Element of TRn;
reconsider X=x as Element of REAL n by EUCLID:22;
0 = nN.x by A4,A5,A6,FUNCT_1:47
.= |.X.| by JGRAPH_4:def 1;
then x=0*n by EUCLID:8;
then x=0.TRn by EUCLID:70;
then x in {0.TRn} by TARSKI:def 1;
hence contradiction by A3,A5,XBOOLE_0:def 5;
end;
then reconsider nN0=nN|TRn0 as non-empty continuous Function of TRn0,R^1
by RELAT_1:def 9;
reconsider b=InN0 as Function of TRn0,TRn by TOPREALC:46;
A7: Int A in the topology of TRn by PRE_TOPC:def 2;
set En=Euclid n,TM=TopSpaceMetr En;
assume that
A8: p in A
and
A9: for r st r>0 ex U be open Subset of TRn|A st p in U & U c= Ball(p,r)
& for f be Function of (TRn) | (A\U),Tunit_circle(n) st f is continuous
ex h be Function of TRn |A,Tunit_circle(n) st
h is continuous & h| (A\U) = f;
reconsider e=p as Point of En by EUCLID:67;
A10:the TopStruct of TRn = TM by EUCLID:def 8;
then reconsider IA=Int A as Subset of TM;
TS = Tcircle(0.TRn,1) by TOPREALB:def 7;
then TS=TRn|S by TOPREALB:def 6;
then
A11: [#]TS=S by PRE_TOPC:def 5;
assume
not p in Fr A;
then p in A\Fr A by A8,XBOOLE_0:def 5;
then p in Int A by TOPS_1:40;
then consider r being Real such that
A12: r > 0
and
A13: Ball(e,r) c= IA by A7,A10,PRE_TOPC:def 2,TOPMETR:15;
set r2=r/2;
consider U be open Subset of TRn|A such that
A14: p in U
and
A15: U c= Ball(p,r2)
and
A16: for f be Function of (TRn) | (A\U),TS st f is continuous
ex h be Function of TRn |A,TS st h is continuous & h| (A\U) = f
by A12, A9;
reconsider Sph=Sphere(p,r2) as non empty Subset of TRn by A1, A12;
consider au be object such that
A17: au in Sph by XBOOLE_0:def 1;
A18:n in NAT by ORDINAL1:def 12;
A19: Ball(e,r)=Ball(p,r) by TOPREAL9:13;
A20: cl_Ball(p,r2) c= Ball(p,r) by JORDAN:21,A18, A12,XREAL_1:216;
A21: Sph = cl_Ball(p,r2) \ Ball(p,r2) by JORDAN:19,A18;
then W: au in cl_Ball(p,r2) by A17,XBOOLE_0:def 5;
A22: au in IA by W,A20,A19,A13;
reconsider r2 as non zero Real by A12;
reconsider CL2=cl_Ball(p,r2) as non empty Subset of TRn by A12;
A23: Sph c= CL2 by A21,XBOOLE_1:36;
[#](TRn|CL2)= CL2 by PRE_TOPC:def 5;
then reconsider sph=Sph as non empty Subset of TRn|CL2 by A21,XBOOLE_1:36;
A24:(TRn|CL2) |sph = TRn|Sph by PRE_TOPC:7, A21,XBOOLE_1:36;
not au in U by A15, A21,A17,XBOOLE_0:def 5;
then reconsider AU=A\U as non empty Subset of TRn by A22,A2,XBOOLE_0:def 5;
set TAU=TRn | AU;
set t= transl(-p,TRn),T= t| TAU;
A25: [#]TAU = A\U by PRE_TOPC:def 5;
then
A26: dom T = A\U by FUNCT_2:def 1;
A27: T=t|the carrier of TAU by TMAP_1:def 4;
A28:rng T c= cTR0
proof
let y be object;
assume y in rng T;
then consider x be object such that
A29: x in dom T
and
A30: T.x=y by FUNCT_1:def 3;
reconsider x as Point of TRn by A29,A26;
A31: T.x=t.x by A29,A27,FUNCT_1:47;
A32: t.x= x+-p by RLTOPSP1:def 10;
assume not y in cTR0;
then T.x in {0.TRn} by A31,XBOOLE_0:def 5,A30;
then x-p = 0.TRn by TARSKI:def 1,A32,A31;
then x= p by RLVECT_1:21;
hence thesis by A29, A25,XBOOLE_0:def 5, A14;
end;
then reconsider T0=T as continuous Function of TAU, TRn0
by A26,FUNCT_2:2,A3,A25,PRE_TOPC:27;
A33: [#](TRn|Sph) = Sph by PRE_TOPC:def 5;
A34:CL2 c= IA by A20,A19,A13;
A35:CL2 c= A by A2,A20,A19,A13;
A36:dom b = cTR0 by A3,FUNCT_2:def 1;
A37: for p be Point of TRn st p in cTR0 holds
b.p=1/|.p.|*p & |.(1/|.p.|)*p.|=1
proof
let p be Point of TRn;
A38: |. 1/|.p.| .|=1/|.p.| by ABSVALUE:def 1;
assume
A39: p in cTR0;
then
A40: I.p=p by A3,TMAP_1:84;
A41:nN0.p=nN.p by A39,A3,A4,FUNCT_1:49;
thus b.p = I.p(/)nN0.p by A36,A39,VALUED_2:72
.= p(/)|.p.| by A41,A40,JGRAPH_4:def 1
.= 1/|.p.|*p by VALUED_2:def 32;
A42:p<>0.TRn by A39,ZFMISC_1:56;
thus |.(1/|.p.|)*p.| = |. 1/|.p.| .|*|.p.| by TOPRNS_1:7
.= 1 by A38,A42,TOPRNS_1:24,XCMPLX_1:87;
end;
rng b c=S
proof
let y be object;
assume y in rng b;
then consider x be object such that
A43: x in dom b
and
A44: b.x=y by FUNCT_1:def 3;
reconsider x as Point of TRn by A36,A43;
A45: |.(1/|.x.|)*x.|=1 by A3,A37,A43;
A46: (1/|.x.|)*x-0.TRn=(1/|.x.|)*x by RLVECT_1:13;
y = 1/|.x.|*x by A3,A37,A43,A44;
hence thesis by A46,A45;
end;
then reconsider B=b as Function of TRn0,TS by A3,A11,A36,FUNCT_2:2;
A47:[#](TRn|CL2|sph )=sph by PRE_TOPC:def 5;
set m = mlt(r2,TRn), M= m|TS;
reconsider M= m|TS as continuous Function of TS,TRn by A1;
A48:M=m|the carrier of TS by TMAP_1:def 4;
A49: [#](TRn|A) = A by PRE_TOPC:def 5;
then reconsider clB= CL2 as Subset of TRn|A by A34,A2,XBOOLE_1:1;
A50:(TRn|A) |clB = TRn|CL2 by PRE_TOPC:7, A34,A2,XBOOLE_1:1;
B is continuous by PRE_TOPC:27;
then B*T0 is continuous by TOPS_2:46;
then consider h be Function of TRn |A,TS such that
A51: h is continuous
and
A52: h| (A\U) = B*T0 by A16;
M*h is continuous Function of TRn|A,TRn by A1,A51,TOPS_2:46;
then reconsider GHM=G*(M*h) as continuous Function of TRn|A,TRn
by TOPS_2:46;
A53:dom h = the carrier of (TRn|A) by A1,FUNCT_2:def 1;
A54: |.r2.|=r2 by A12,ABSVALUE:def 1;
A55:rng GHM c= Sph
proof
let y be object;
assume y in rng GHM;
then consider q be object such that
A56: q in dom GHM
and
A57: GHM.q=y by FUNCT_1:def 3;
A58:y = G.((M*h).q) by A56,A57,FUNCT_1:12;
A59:q in A by A56,A49;
A60:q in dom (M*h) by A56,FUNCT_1:11;
then
A61: q in dom h by FUNCT_1:11;
A62:(M*h).q=M.(h.q) by A60,FUNCT_1:12;
A63:h.q in dom M by A60,FUNCT_1:11;
reconsider q as Point of TRn by A59;
h.q in S by A63,A11;
then reconsider hq=h.q as Point of TRn;
A64:m.(h.q) = r2 * hq by RLTOPSP1:def 13;
M.(h.q)=m.(h.q) by A63,A48,FUNCT_1:47;
then
A65: y = p+(r2*hq) by A58,A62,A64,RLTOPSP1:def 10;
A66:p+(r2*hq) - p = (r2*hq )+(p - p) by RLVECT_1:28
.= (r2*hq)+(0.TRn) by RLVECT_1:15
.= r2*hq by RLVECT_1:def 4;
A67:h.q in rng h by FUNCT_1:def 3,A61;
|. r2 * hq.| = |. r2 .| * |. hq .| by EUCLID:11
.= |.r2.| *1 by A67,A11,TOPREAL9:12;
hence thesis by A66,A65,A54;
end;
dom GHM = A by A49,FUNCT_2:def 1;
then reconsider ghm=GHM as Function of TRn|A,TRn|Sph
by A55,A49,A33,FUNCT_2:2;
ghm is continuous by PRE_TOPC:27;
then reconsider ghM=ghm| ((TRn|A) |clB ) as continuous
Function of TRn|CL2,(TRn|CL2) |sph by A8,A50,A24;
A68:dom ghM = the carrier of (TRn|CL2) by FUNCT_2:def 1;
A69:ghM =ghm|the carrier of ((TRn|A) |clB ) by TMAP_1:def 4, A8;
for w be Point of TRn|CL2 st w in Sph holds ghM.w=w
proof
let w be Point of TRn|CL2;
assume
A70: w in Sph;
then reconsider q=w as Point of TRn;
A71:w in CL2 by A70,A23;
w in A by A35,A70,A23;
then
A72: q in dom GHM by A49,FUNCT_2:def 1;
then
A73: q in dom (M*h) by FUNCT_1:11;
then
A74: (M*h).q=M.(h.q) by FUNCT_1:12;
not q in U by A70,A21,XBOOLE_0:def 5,A15;
then
A75: q in A\U by A71,A35,XBOOLE_0:def 5;
then q in (A\U) /\ dom h by A71,A35,A53,A49,XBOOLE_0:def 4;
then
A76: q in dom (B*T0) by A52,RELAT_1:61;
then
A77: (B*T0).q = B.(T0.q) by FUNCT_1:12;
A78:h.q in dom M by A73,FUNCT_1:11;
then
A79:M.(h.q)=m.(h.q) by A48,FUNCT_1:47;
t.q = q+-p by RLTOPSP1:def 10;
then
A80: T.q=q-p by A26,A27,A75,FUNCT_1:47;
q in dom T0 by A76,FUNCT_1:11;
then
A81: T.q in rng T by FUNCT_1:def 3;
h.q in S by A78,A11;
then reconsider hq=h.q as Point of TRn;
ghM.q=ghm.q by A68,A69, FUNCT_1:47;
then
A82: ghM.q = G.((M*h).q) by A72,FUNCT_1:12;
hq = (B*T0).q by A76,A52,FUNCT_1:47;
then
A83: hq=1/|.q-p.|*(q-p) by A80,A77,A37, A81,A28;
m.(h.q) = r2 * hq by RLTOPSP1:def 13
.= r2 *(1/r2*(q-p)) by A83, A70,TOPREAL9:9
.= (r2*(1/r2))*(q-p) by RLVECT_1:def 7
.= 1 *(q-p) by XCMPLX_1:106
.= q-p by RLVECT_1:def 8;
then ghM.w = p+(q-p ) by A82,A74,A79,RLTOPSP1:def 10
.= q +(-p+p) by RLVECT_1:def 3
.=q + 0.TRn by RLVECT_1:def 10
.= q by RLVECT_1:4;
hence thesis;
end;
then
A84:ghM is being_a_retraction by BORSUK_1:def 16,A33,A24;
Ball(p,r2) c= Int CL2 by TOPREAL9:16,TOPS_1:24;
then
A85: CL2 is non boundary by A12;
Fr CL2 = Sph by A12,BROUWER2:5;
hence
contradiction by A84,A85,A47,BROUWER2:9,BORSUK_1:def 17;
end;
theorem Th9:
for p st p in Fr A & A is closed
for r st r>0
ex U be open Subset of (TOP-REAL n) |A st
p in U & U c= Ball(p,r) &
for f be Function of (TOP-REAL n) | (A\U),Tunit_circle(n) st
f is continuous
ex h be Function of (TOP-REAL n) |A,Tunit_circle(n) st
h is continuous & h| (A\U) = f
proof
set TR=TOP-REAL n;
let p;
assume that
A1: p in Fr A
and
A2: A is closed;
A3:Fr A c= A by TOPS_1:35, A2;
n>0
proof
assume n<=0;
then n=0;
then
A4: the carrier of TR = {0.TR} by EUCLID:77,22;
[#]TR is open;
hence thesis by A4, A1,ZFMISC_1:33;
end;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
set TU=Tunit_circle(n);
A5: p is Element of REAL n by EUCLID:22;
let r;
assume
A6: r>0;
set r3=r/3,r2=2*r3;
set B=Ball(p,r3);
p is Element of REAL n by EUCLID:22;
then |. p-p .|=0;
then p in B by A6;
then A` meets B by A1,TOPS_1:28;
then consider x be object such that
A7: x in A`
and
A8: x in B by XBOOLE_0:3;
reconsider x as Element of TR by A7;
set u=Ball(x,r2), clU=cl_Ball(x,r2);
A9:n in NAT by ORDINAL1:def 12;
A10:u c= clU by TOPREAL9:16;
A11:[#](TR|A)=A by PRE_TOPC:def 5;
then reconsider U=u/\A as Subset of TR|A by XBOOLE_1:17;
u in the topology of TR by PRE_TOPC:def 2;
then U in the topology of TR|A by PRE_TOPC:def 4,A11;
then reconsider U as open Subset of TR|A by PRE_TOPC:def 2;
take U;
x is Element of REAL n by EUCLID:22;
then
A12: |.x-p.| =|.p-x.| by EUCLID:18, A5;
|.x-p.|+r2 < r3+r2 by A8,TOPREAL9:7,XREAL_1:6;
then
A13: u c= Ball(p,r) by Th5;
r2 > r3 by A6,XREAL_1:155;
then |.x-p.| < r2 by A8,TOPREAL9:7,XXREAL_0:2;
then
A14: p in u by A12;
hence p in U by A3, A1,XBOOLE_0:def 4;
U c= u by XBOOLE_1:17;
hence U c= Ball(p,r) by A13;
let f be Function of TR | (A\U),TU such that
A15: f is continuous;
per cases;
suppose
A16: A\U is empty;
set h = the continuous Function of TR |A,Tunit_circle(n1+1);
reconsider H=h as Function of (TOP-REAL n) |A,TU;
take H;
f={} by A16;
hence thesis by A16;
end;
suppose
A17: A\U is non empty;
set S = Sphere(x,r2);
reconsider AUS=(A\U)\/S as non empty Subset of TR by A17;
A18: TR|AUS is metrizable & TR|AUS is finite-ind second-countable
proof
reconsider aus=AUS as Subset of the TopStruct of TR;
A19: the TopStruct of TR = TopSpaceMetr Euclid n by EUCLID:def 8;
TR|AUS = (the TopStruct of TR) |aus by PRE_TOPC:36;
hence thesis by A19;
end;
A20: [#] (TR|AUS) = AUS by PRE_TOPC:def 5;
then reconsider AU=A\U,SS=S as Subset of TR|AUS by XBOOLE_1:7;
AU` = (AUS)\AU by SUBSET_1:def 4,A20
.= S\AU by XBOOLE_1:40;
then
A21: AU` c= SS by XBOOLE_1:36;
ind S = n1 by A6,Th7;
then ind SS =n1 by TOPDIM_1:21;
then
A22: ind (AU`) <= n1 by TOPDIM_1:19,A21;
A23: TR| (A\U) = TR|AUS| (AU) by A20,PRE_TOPC:7;
then reconsider F=f as Function of TR |AUS| AU,TU;
A\U = A\u by XBOOLE_1:47;
then
A24: A\U is closed by A2,YELLOW_8:20;
then AU is closed by TSEP_1:8;
then consider g be continuous Function of TR |AUS, Tunit_circle(n1+1)
such that
A25: g|AU=F by Th3, A23,A15, A18,A22;
A26: [#](TR|A) = A by PRE_TOPC:def 5;
then reconsider AclU=A/\clU, au=A\U as Subset of TR|A by XBOOLE_1:17,36;
set T3=TR |A | AclU, T4=TR |A | au;
A27: (A/\U) \/ au = A by XBOOLE_1:51;
A`= ([#]TR)\A by SUBSET_1:def 4;
then not x in A by A7,XBOOLE_0:def 5;
then consider h be Function of TR |A,TR |S such that
A28: h is continuous
and
A29: h|S = id (A/\S) by A6,Th4;
A30: n1+1 = n;
then
A31: dom h = the carrier of (TR|A) by A6,FUNCT_2:def 1;
A32: [#](TR|S)=S by PRE_TOPC:def 5;
then rng h c= the carrier of TR by XBOOLE_1:1;
then reconsider h1=h as Function of TR|A,TR by A31,FUNCT_2:2;
A33: S c= AUS by XBOOLE_1:7;
rng h c= [#](TR|S);
then reconsider h2=h1 as Function of TR|A,TR|AUS
by A33,A32,XBOOLE_1:1,A31,FUNCT_2:2,A20;
h1 is continuous by A28,PRE_TOPC:26;
then
A34: h2 is continuous by PRE_TOPC:27;
set T2=TR |AUS|AU;
A35: TR |AUS | AU = TR| (A\U) by PRE_TOPC:7, XBOOLE_1:7;
A36: clU\u = S by JORDAN:19,A9;
A37: (A/\A)/\u = A/\(A/\u) by XBOOLE_1: 16;
A38: g|T2 = g|the carrier of T2 by TMAP_1:def 4;
TR |A | au = TR| (A\U) by XBOOLE_1:36,PRE_TOPC:7;
then reconsider gT2=g|T2 as continuous Function of T4,Tunit_circle(n1+1)
by A35,A17;
A39: [#]T3 =AclU by PRE_TOPC:def 5;
AclU is non empty by A10,A14, A3, A1,XBOOLE_0:def 4;
then reconsider gh2T3=g*(h2|T3) as continuous
Function of T3,Tunit_circle(n1+1) by A34;
A40: [#]T4 = au by PRE_TOPC:def 5;
A41: h2|T3 = h2|the carrier of T3 by A3, A1, TMAP_1:def 4;
A42: now
let x be object such that
A43: x in dom gh2T3 /\ dom gT2;
A44: not x in U by A43,A40,XBOOLE_0:def 5;
x in A by A43,A40,XBOOLE_0:def 5;
then
A45: not x in u by A44,XBOOLE_0:def 4;
A46: x in dom gh2T3 by A43,XBOOLE_0:def 4;
then x in clU by A39,XBOOLE_0:def 4;
then
A47: x in S by A45,A36,XBOOLE_0:def 5;
A48: x in dom gT2 by A43,XBOOLE_0:def 4;
x in A by A46,A39,XBOOLE_0:def 4;
then
A49: x in A/\S by A47,XBOOLE_0:def 4;
x in dom (h2|T3) by A46,FUNCT_1:11;
then (h2|T3).x = h2.x by A41,FUNCT_1:47
.= (h|S).x by A47,FUNCT_1:49
.= x by A29,A49,FUNCT_1:17;
hence gh2T3.x = g.x by A46,FUNCT_1:12
.= gT2.x by A38,A48,FUNCT_1:47;
end;
A50: AclU is closed by A2,TSEP_1:8;
au is closed by A24,TSEP_1:8;
then reconsider G=gh2T3+* gT2 as continuous
Function of TR|A| ( AclU\/au),Tunit_circle(n1+1)
by A50,A42,PARTFUN1:def 4,TOPGEN_5:10;
W: A/\u c= AclU by TOPREAL9:16,XBOOLE_1:26;
A = AclU\/au by A26,W,A27,A37,XBOOLE_1:9;
then
A51: TR|A| (AclU\/au) = TR|A by A26,TSEP_1:93;
then reconsider GG=G as Function of TR|A, TU;
take GG;
thus GG is continuous by A51;
A52: [#](TR| (A\U)) = A\U by PRE_TOPC:def 5;
A53: dom gT2 =the carrier of T4 by FUNCT_2:def 1;
A54: now let x;
assume
A55: x in dom f;
hence (GG| (A\U)).x = GG.x by A52,FUNCT_1:49
.= gT2.x by FUNCT_4:13, A55,A52,A40,A53
.= g.x by A38,A40,A52,A53,A55,FUNCT_1:47
.= f.x by A25, A55,A52,FUNCT_1:49;
end;
dom GG = A by A26,FUNCT_2:def 1;
then
A56: dom (GG| (A\U)) = A /\ ( A\U) by RELAT_1:61
.= A\U by XBOOLE_1:36,XBOOLE_1:28;
dom f = A\U by A30,A52,FUNCT_2:def 1;
hence thesis by A54,A56;
end;
end;
Lm3: for A,B be Subset of TOP-REAL n st n = 0
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism
for p be Point of TOP-REAL n
holds (p in Fr A implies h.p in Fr B) &
(p in Int A implies h.p in Int B)
proof
set TR=TOP-REAL n;
A1: Int ([#]TR)=[#]TR by TOPS_1:15;
let A,B be Subset of TR such that
A2: n = 0;
A3:the carrier of TR = {0.TR} by A2,EUCLID:77,22;
let h be Function of TR |A,TR |B such that
A4:h is being_homeomorphism;
A5: dom h = [#](TR|A) by A4, TOPS_2:def 5;
let p be Point of TR;
[#]TR is open;
hence p in Fr A implies h.p in Fr B by A3,ZFMISC_1:33;
A6: A = [#](TR|A) by PRE_TOPC:def 5;
A7: Int A c= A by TOPS_1:16;
assume p in Int A;
then
A8: h.p in rng h by A7,A5,A6,FUNCT_1:def 3;
A9: B=[#](TR|B) by PRE_TOPC:def 5;
then B=[#]TR by A8,ZFMISC_1:33,A3;
hence thesis by A8,A1,A9;
end;
begin :: Brouwer Invariance of Domain Theorem - Special case
theorem Th10:
A is closed & p in Fr A implies
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism
holds h.p in Fr B
proof
set TRn=TOP-REAL n;
assume that
A1: A is closed
and
A2: p in Fr A;
A3:Fr A c= A by A1, TOPS_1:35;
let h be Function of TRn|A,TRn|B such that
A4: h is being_homeomorphism;
A5: [#](TRn|A) = A by PRE_TOPC:def 5;
then
A6: dom h = A by A4,TOPS_2:def 5;
then
A7: h.p in rng h by A3,A2,FUNCT_1:def 3;
A8: [#](TRn|B) = B by PRE_TOPC:def 5;
then
A9: rng h = B by A4,TOPS_2:def 5;
then reconsider hp=h.p as Point of TRn by A7;
per cases;
suppose n=0;
hence thesis by Lm3,A4, A2;
end;
suppose
A10: n>0;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
A11: the TopStruct of TRn=TopSpaceMetr Euclid n by EUCLID:def 8;
for r st r>0 ex U be open Subset of TRn|B st
hp in U & U c= Ball(hp,r) &
for f be Function of TRn | (B\U),Tunit_circle(n) st
f is continuous ex h be Function of TRn |B,Tunit_circle(n) st
h is continuous & h| (B\U) = f
proof
reconsider P =p as Point of Euclid n by A11, TOPMETR:12;
let r such that
A13: r>0;
reconsider BB=B/\Ball(hp,r) as Subset of TRn|B by A8,XBOOLE_1:17;
Ball(hp,r) in the topology of TRn by PRE_TOPC:def 2;
then BB in the topology of (TRn|B) by A8,PRE_TOPC:def 4;
then reconsider BB as open Subset of TRn|B by PRE_TOPC:def 2;
h"BB is open by A7,A4,A8, TOPS_2:43;
then h"BB in the topology of TRn|A by PRE_TOPC:def 2;
then consider U be Subset of TRn such that
A14: U in the topology of TRn
and
A15: h"BB = U/\[#](TRn|A) by PRE_TOPC:def 4;
reconsider U as open Subset of TRn by A14,PRE_TOPC:def 2;
A16: Int U = U by TOPS_1:23;
hp is Element of REAL n by EUCLID:22;
then |. hp-hp .|=0;
then hp in Ball(hp,r) by A13;
then hp in BB by A7,A8,XBOOLE_0:def 4;
then p in h"BB by A3,A2, A6,FUNCT_1:def 7;
then p in U by A15,XBOOLE_0:def 4;
then consider s be Real such that
A17: s>0
and
A18: Ball(P,s) c= U by A16,GOBOARD6:5;
consider W be open Subset of TRn|A such that
A19: p in W
and
A20: W c= Ball(p,s)
and
A21: for f be Function of TRn | (A\W),Tunit_circle(n) st
f is continuous ex h be Function of
(TOP-REAL n) |A,Tunit_circle(n)
st h is continuous & h| (A\W) = f by A1,A17,Th9, A2;
Ball(p,s)=Ball(P,s) by TOPREAL9:13;
then
A22: Ball(p,s)/\A c= U/\A by A18, XBOOLE_1: 27;
W/\A=W by A5,XBOOLE_1:28;
then W c= Ball(p,s)/\A by A20, XBOOLE_1: 27;
then W c= U/\A by A22;
then h.:W c= h.:(U/\A) by RELAT_1:123;
then
A23: h.:W c= BB by FUNCT_1:77,A8,A9,A15,A5;
TRn|B is non empty by A3,A2, A6;
then
reconsider hW=h.:W as open Subset of TRn|B by A3,A2,A4,TOPGRP_1:25;
take hW;
BB c= Ball(hp,r) by XBOOLE_1:17;
hence hp in hW & hW c= Ball(hp,r)
by A3,A2,A6,FUNCT_1:def 6,A19,A23;
set AW=A\W,haw=h| AW,T=Tunit_circle(n);
A24: [#](TRn | (B\hW))=B\hW by PRE_TOPC:def 5;
reconsider aw=AW as Subset of TRn|A by XBOOLE_1:36,A5;
let f be Function of TRn | (B\hW),T such that
A25: f is continuous;
per cases;
suppose
A26: B\hW is empty;
set h = the continuous Function of TRn |B,Tunit_circle(n1+1);
reconsider H=h as Function of (TOP-REAL n) |B,T;
take H;
f={} by A26;
hence thesis by A26;
end;
suppose
A27: B\hW is non empty;
set AW=A\W,haw=h| AW,T=Tunit_circle(n);
reconsider haw as Function of (TRn |A) | aw,(TRn|B) | (h.:AW)
by A3,A2,A7,JORDAN24:12;
A28: h.:AW = (h.:A) \ (h.:W) by A4, FUNCT_1:64
.= B\hW by RELAT_1:113,A6,A9;
then
A29: (TRn|B) | (h.:AW) = TRn | (B\hW) by XBOOLE_1:36,PRE_TOPC:7;
A30: (TRn |A) | aw = TRn |AW by PRE_TOPC:7, XBOOLE_1:36;
then reconsider HAW =haw as Function of TRn |AW,TRn | (B\hW)
by A29;
reconsider fhW=f*HAW as Function of TRn | AW,Tunit_circle(n)
by A27;
fhW is continuous
by A27,JORDAN24:13,A4,A3,A2,A7,A29,A30,A25,TOPS_2:46;
then consider HW be Function of TRn |A,T such that
A31: HW is continuous
and
A32: HW| AW = fhW by A21;
reconsider HWh=HW*(h") as Function of TRn|B,T by A3,A2;
take HWh;
h" is continuous by A4,TOPS_2:def 5;
hence HWh is continuous by TOPS_2:46, A3,A2,A31;
A33: dom f = B\hW by A10,A24, FUNCT_2:def 1;
A34: rng ((h") | (B \ hW)) = (h").:(B\hW) by RELAT_1:115
.= h"(h.:AW ) by A28,A8,A9,A4,TOPS_2:55
.= AW by FUNCT_1:94,A6,A4,XBOOLE_1:36;
thus HWh | (B \ hW) = HW* ((h") | (B \ hW)) by RELAT_1:83
.= HW * ((id (AW))*((h") | (B \ hW))) by A34, RELAT_1:53
.= (HW * (id (AW)))*((h") | (B \ hW)) by RELAT_1:36
.= (HW |AW)*((h") | (B \ hW)) by RELAT_1:65
.=( (f*h) |AW ) * ((h") | (B \ hW)) by A32,RELAT_1:83
.=( (f*h) *(id AW )) * ((h") | (B \ hW)) by RELAT_1:65
.= (f*h) *((id AW ) * ((h") | (B \ hW))) by RELAT_1:36
.= (f*h) *( (h") | (B \ hW)) by A34,RELAT_1:53
.= ((f*h) * (h")) | (B \ hW) by RELAT_1:83
.= (f*(h * h")) | (B \ hW) by RELAT_1:36
.= (f*id B) | (B \ hW) by TOPS_2:52,A9, A4, A8
.= f | (dom f) by A33, XBOOLE_1:36,RELAT_1:51
.=f;
end;
end;
hence thesis by Th8, A7,A8, A10;
end;
end;
theorem Th11:
B is closed & p in Int A implies
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism holds h.p in Int B
proof
set TRn=TOP-REAL n,T=Tunit_circle(n);
assume that
A1: B is closed
and
A2: p in Int A;
A3: Int A c= A by TOPS_1:16;
A4: the TopStruct of TRn=TopSpaceMetr Euclid n by EUCLID:def 8;
let h be Function of TRn|A,TRn|B such that
A5: h is being_homeomorphism;
A6: h" is continuous by A5,TOPS_2:def 5;
A7: [#](TRn|A) = A by PRE_TOPC:def 5;
then A8: dom h = A by A5,TOPS_2:def 5;
A9: [#](TRn|B) = B by PRE_TOPC:def 5;
then A10: rng h = B by A5,TOPS_2:def 5;
per cases;
suppose n=0;
hence thesis by Lm3,A2,A5;
end;
suppose
A11: n>0;
A12: h.p in rng h by A2,A3,A8,FUNCT_1:def 3;
then reconsider hp=h.p as Point of TRn by A10;
ex r st r>0 & for U be open Subset of TRn |B st
hp in U & U c= Ball(hp,r) ex f be Function of TRn | (B\U),T st
f is continuous & for h be Function of TRn |B,T
st h is continuous holds h| (B\U) <> f
proof
reconsider hP =hp as Point of Euclid n by A4, TOPMETR:12;
not p in Fr A by A2, TOPS_1:39,XBOOLE_0:3;
then consider r such that
A14: r>0
and
A15: for U be open Subset of TRn |A st p in U & U c= Ball(p,r)
ex f be Function of TRn | (A\U),T st f is continuous &
for h be Function of TRn |A,T st h is continuous holds
h| (A\U) <> f by A11, A2,A3,Th8;
reconsider BA=Ball(p,r) /\A as Subset of TRn|A by A7,XBOOLE_1: 17;
Ball(p,r) in the topology of TRn by PRE_TOPC:def 2;
then BA in the topology of (TRn|A) by A7,PRE_TOPC:def 4;
then reconsider BA as open Subset of TRn|A by PRE_TOPC:def 2;
h.:BA is open by A5,A2,A3,A12, TOPGRP_1:25;
then h.:BA in the topology of TRn|B by PRE_TOPC:def 2;
then consider U be Subset of TRn such that
A16: U in the topology of TRn
and
A17: h.:BA = U/\[#](TRn|B) by PRE_TOPC :def 4;
reconsider U as open Subset of TRn by A16,PRE_TOPC:def 2;
A18: Int U = U by TOPS_1:23;
p is Element of REAL n by EUCLID:22;
then |. p-p .|=0;
then p in Ball(p,r) by A14;
then p in BA by A2,A3,XBOOLE_0:def 4;
then hp in h.:BA by A7,A8,FUNCT_1:def 6;
then hp in U by A17,XBOOLE_0:def 4;
then consider s be Real such that
A19: s>0
and
A20: Ball(hP,s) c= U by A18,GOBOARD6:5;
take s;
thus s>0 by A19;
let W be open Subset of TRn |B such that
A21: hp in W
and
A22: W c= Ball(hp,s);
A23: W/\B=W by A9,XBOOLE_1:28;
Ball(hp,s)=Ball(hP,s) by TOPREAL9:13;
then W c= U by A22,A20;
then
A24: W c= U/\B by A23, XBOOLE_1:27;
h"(U/\B) = h"(h.:BA ) by A17, PRE_TOPC:def 5
.= BA by FUNCT_1:94, XBOOLE_1:17,A8, A5;
then
A25: h"W c= BA by A24,RELAT_1:143;
reconsider hW=h"W as open Subset of TRn|A by TOPS_2:43,A5,A9,A12;
A26: BA c= Ball(p,r) by XBOOLE_1:17;
set BW=B\W;
reconsider bw=BW as Subset of TRn|B by XBOOLE_1:36,A9;
A27: [#](TRn | (A\hW))=A\hW by PRE_TOPC:def 5;
p in h"W by A8,A2,A3,A21,FUNCT_1:def 7;
then consider F be Function of TRn | (A\hW),T such that
A28: F is continuous
and
A29: for h be Function of TRn |A,T st h is continuous holds
h| (A\hW) <> F by A15, A25,A26,XBOOLE_1:1;
A30: BW c= B by XBOOLE_1:36;
then
A31: h".:BW = h"BW by TOPS_2:55,A9,A10, A5
.= (h"B) \ hW by FUNCT_1:69
.=A\hW by RELAT_1:134,A8,A10;
per cases;
suppose
A32: A\hW is empty;
reconsider n1=n-1 as Element of NAT by NAT_1:20, A11;
set h = the continuous Function of TRn |A,Tunit_circle(n1+1);
reconsider H=h as Function of TRn |A,T;
A33: H| (A\hW) = {} by A32;
H| (A\hW) <> F by A29;
hence thesis by A33, A32;
end;
suppose
A34: A\hW is non empty;
reconsider hbw=(h") | (B\W) as Function of
(TRn |B) | bw, (TRn|A) | (h".:BW) by A2,A3,A12,JORDAN24:12;
A35: (TRn |B) | bw = TRn |BW by PRE_TOPC:7, XBOOLE_1:36;
A36: (TRn|A) | (h".:BW) = TRn | (A\hW) by A31, PRE_TOPC:7,A7;
then reconsider HBW =hbw as Function of TRn |BW, TRn | (A\hW)
by A35;
reconsider fhW=F*HBW as Function of TRn | BW,Tunit_circle(n)
by A34;
take fhW;
thus fhW is continuous by A34,JORDAN24:13,
A6,A2,A3,A12,A36,A35,A28,TOPS_2:46;
let g be Function of TRn |B,T such that
A37: g is continuous;
reconsider gh=g*h as Function of TRn |A,T by A12;
A38: gh is continuous by A5, A12,A37,TOPS_2:46;
assume
A39: g| BW = fhW;
A40: dom F = A\hW by FUNCT_2:def 1, A11,A27;
A41: rng (h| (A\hW)) = h.:(A\hW) by RELAT_1:115
.=h.:(h"BW) by TOPS_2:55,A9,A10,A31, A5,A30
.=BW by FUNCT_1:77,A10, XBOOLE_1:36;
gh| (A\hW) = g*(h| (A\hW)) by RELAT_1:83
.=g*((id BW)*(h| (A\hW))) by A41,RELAT_1:53
.=(g*(id BW))*(h| (A\hW)) by RELAT_1:36
.=(g|BW)*(h| (A\hW)) by RELAT_1:65
.=F*(((h") | (B\W)) * (h| (A\hW))) by A39, RELAT_1:36
.=F*(((h") *id BW) * (h| (A\hW))) by RELAT_1:65
.=F*((h") *(id BW * (h| (A\hW)))) by RELAT_1:36
.=F*((h") * (h| (A\hW))) by A41,RELAT_1:53
.=F*((h" * h) | (A\hW)) by RELAT_1:83
.=(F*(h" * h)) | (A\hW) by RELAT_1:83
.=(F*(id A)) | (A\hW) by TOPS_2:52,A8,A10, A5,A9
.=F | dom F by A40, XBOOLE_1:36,RELAT_1:51
.=F;
hence contradiction by A38,A29;
end;
end;
then not hp in Fr B by A1,Th9;
then hp in B\Fr B by A12,A9,XBOOLE_0:def 5;
hence thesis by TOPS_1:40;
end;
end;
theorem
A is closed & B is closed implies
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism
holds h.:Int A = Int B & h.:Fr A = Fr B
proof
assume that
A1: A is closed
and
A2: B is closed;
set TR=TOP-REAL n;
A3: [#](TR|A) = A by PRE_TOPC:def 5;
A4: Int B c= B by TOPS_1:16;
A5: [#](TR|B)=B by PRE_TOPC:def 5;
let h be Function of TR |A,TR |B such that
A6: h is being_homeomorphism;
A7: dom h = [#](TR|A) by A6,TOPS_2:def 5;
A8: rng h = [#](TR|B) by A6,TOPS_2:def 5;
A9: Fr A \/Int A = (A \Int A) \/Int A by A1,TOPS_1:43
.= A\/Int A by XBOOLE_1:39
.= A by TOPS_1:16,XBOOLE_1:12;
thus
A10: h.:Int A = Int B
proof
thus h.:Int A c= Int B
proof
let y be object;
assume y in h.:Int A;
then ex x be object st x in dom h & x in Int A & h.x=y
by FUNCT_1:def 6;
hence thesis by A2,A6,Th11;
end;
let y be object;
assume
A11: y in Int B;
then consider x be object such that
A12: x in dom h
and
A13: h.x=y by A4,A8,A5,FUNCT_1:def 3;
reconsider x as Point of TR by A7,A3,A12;
assume
A14: not y in h.:Int A;
not x in Int A by A12,FUNCT_1:def 6,A14,A13;
then x in Fr A by A12,A9,A3,XBOOLE_0:def 3;
then h.x in Fr B by Th10,A1,A6;
hence thesis by A11,A13, TOPS_1:39,XBOOLE_0:3;
end;
Fr A = A \Int A by A1,TOPS_1:43;
then h.:Fr A = (h.:A) \ (h.:Int A) by A6,FUNCT_1:64
.= B\ (h.:Int A) by RELAT_1:113,A7,A8,A3,A5
.= Fr B by A10,A2,TOPS_1:43;
hence thesis;
end;
begin :: Topological Invariance of Dimension - An Introduction to Manifolds
theorem Th13:
for r st r>0
for U be Subset of Tdisk(p,r) st U is open non empty
for A be Subset of TOP-REAL n st A = U holds Int A is non empty
proof
set TR=TOP-REAL n;
let r be Real such that
A1: r>0;
let U be Subset of Tdisk(p,r) such that
A2: U is open non empty;
consider q be object such that
A3: q in U by A2;
A4: [#]Tdisk(p,r) = cl_Ball(p,r) by PRE_TOPC:def 5;
then q in cl_Ball(p,r) by A3;
then reconsider q as Point of TR;
the TopStruct of TR=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider Q=q as Point of Euclid n by TOPMETR:12;
A5: |.q-p.|<= r by A3,A4,TOPREAL9:8;
U in the topology of Tdisk(p,r) by A2,PRE_TOPC:def 2;
then consider W be Subset of TR such that
A6: W in the topology of TR
and
A7: U = W /\ [#]Tdisk(p,r) by PRE_TOPC:def 4;
reconsider W as open Subset of TR by A6,PRE_TOPC:def 2;
Int W=W by TOPS_1:23;
then q in Int (W) by A3,A7,XBOOLE_0:def 4;
then consider s be Real such that
A8: s>0
and
A9: Ball(Q,s) c= W by GOBOARD6:5;
set m=min(s,r),mr=m/(2*r);
A10: 0< m by A8,A1, XXREAL_0:21;
then
A11: m/2 < m by XREAL_1:216;
set qp = (-mr)*(q-p)+q;
A12: qp -q = (-mr)*(q-p)+(q-q) by RLVECT_1:def 3
.=(- mr)*(q-p)+0.TR by RLVECT_1:def 10
.=(-mr)*(q-p) by RLVECT_1:def 4;
|.-mr.| =--mr by A10, A1,ABSVALUE:def 1;
then
A13: |.qp-q.| = mr *|.q-p.| by A12,EUCLID:11;
mr *r = m/2/r*r by XCMPLX_1:78
.= m/2*(r/r)
.= m/2*1 by XCMPLX_1:60,A1
.= m/2;
then |.qp-q.| <= m/2 by A5,XREAL_1:66, A10,A13;
then
A14: |.qp-q.| < m by A11,XXREAL_0:2;
m <= s by XXREAL_0: 17;
then |.qp-q.| ~~0;
then (1-mr)*|. q-p .| < 1*|. q-p .| by A18,XREAL_1:68;
hence thesis by A5,XXREAL_0:2;
end;
end;
A20: r/(2*r) = r/r/2 by XCMPLX_1:78
.= 1/2 by XCMPLX_1:60,A1;
mr <= r/(2*r) by A1, XXREAL_0:17, XREAL_1:72;
then 1-mr >= 1-1/2 by A20,XREAL_1:10;
then
A21: |.1-mr.|=1-mr by ABSVALUE:def 1;
qp - p =(-mr)*(q-p)+(q-p) by RLVECT_1:def 3
.=(-mr)*(q-p)+1*(q-p) by RLVECT_1:def 8
.=(1-mr)*(q-p) by RLVECT_1:def 6;
then |.qp - p.| ~~