let n be Nat; :: thesis: for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds
for F being closed Subset of TM st ind (F `) <= n holds
for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f
defpred S1[ Nat] means for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds
for F being closed Subset of TM st ind (F `) <= $1 holds
for f being 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; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= n holds
for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f )
assume A1: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= n holds
for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f
let F be closed Subset of TM; :: thesis: ( ind (F `) <= n implies for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f )
assume A2: ind (F `) <= n ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
set n2 = (n + 1) + 1;
assume A4: S1[n] ; :: thesis: S1[n + 1]
set Tn1 = TOP-REAL (n + 1);
set Tn2 = TOP-REAL ((n + 1) + 1);
set U = Tunit_circle ((n + 1) + 1);
let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= n + 1 holds
for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f ) )
assume A5: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= n + 1 holds
for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f )
let F be closed Subset of TM; :: thesis: ( ind (F `) <= n + 1 implies for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f ) )
assume A6: ind (F `) <= n + 1 ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f )
let f be continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)); :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f )
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 ( F is empty or not F is empty ) ;
suppose A11: F is empty ; :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f )
take g = TM --> the Point of (Tunit_circle ((n + 1) + 1)); :: thesis: ( g is continuous & g | F = f )
g | F = {} by A11;
hence ( g is continuous & g | F = f ) by A11; :: thesis: verum
end;
suppose A12: not F is empty ; :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st
( g is continuous & g | F = f )
set Sn = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } ;
set Sp = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } ;
A13: { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } c= the carrier of (TOP-REAL ((n + 1) + 1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } or x in the carrier of (TOP-REAL ((n + 1) + 1)) )
assume x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL ((n + 1) + 1))
then ex p being Point of (TOP-REAL ((n + 1) + 1)) st
( p = x & p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) ;
hence x in the carrier of (TOP-REAL ((n + 1) + 1)) ; :: thesis: verum
end;
{ p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } c= the carrier of (TOP-REAL ((n + 1) + 1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } or x in the carrier of (TOP-REAL ((n + 1) + 1)) )
assume x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL ((n + 1) + 1))
then ex p being Point of (TOP-REAL ((n + 1) + 1)) st
( p = x & p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) ;
hence x in the carrier of (TOP-REAL ((n + 1) + 1)) ; :: thesis: verum
end;
then reconsider Sp = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } , Sn = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } as Subset of (TOP-REAL ((n + 1) + 1)) by A13;
A14: Sn = { t where t is Point of (TOP-REAL ((n + 1) + 1)) : ( t . ((n + 1) + 1) <= 0 & |.t.| = 1 ) } ;
A15: Sp = { l where l is Point of (TOP-REAL ((n + 1) + 1)) : ( l . ((n + 1) + 1) >= 0 & |.l.| = 1 ) } ;
then reconsider s1 = Sp, s2 = Sn as closed Subset of (TOP-REAL ((n + 1) + 1)) by A14, Th2;
A16: [#] ((TOP-REAL ((n + 1) + 1)) | s2) = s2 by PRE_TOPC:def 5;
Tunit_circle ((n + 1) + 1) = Tcircle ((0. (TOP-REAL ((n + 1) + 1))),1) by TOPREALB:def 7;
then A17: the carrier of (Tunit_circle ((n + 1) + 1)) = Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) by TOPREALB:9;
A18: s1 c= the carrier of (Tunit_circle ((n + 1) + 1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s1 or x in the carrier of (Tunit_circle ((n + 1) + 1)) )
assume x in s1 ; :: thesis: x in the carrier of (Tunit_circle ((n + 1) + 1))
then consider p being Point of (TOP-REAL ((n + 1) + 1)) such that
A19: x = p and
p . ((n + 1) + 1) >= 0 and
A20: |.p.| = 1 ;
p - (0. (TOP-REAL ((n + 1) + 1))) = p by RLVECT_1:13;
hence x in the carrier of (Tunit_circle ((n + 1) + 1)) by A20, A19, A17; :: thesis: verum
end;
A21: s2 c= the carrier of (Tunit_circle ((n + 1) + 1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s2 or x in the carrier of (Tunit_circle ((n + 1) + 1)) )
assume x in s2 ; :: thesis: x in the carrier of (Tunit_circle ((n + 1) + 1))
then consider p being Point of (TOP-REAL ((n + 1) + 1)) such that
A22: x = p and
p . ((n + 1) + 1) <= 0 and
A23: |.p.| = 1 ;
p - (0. (TOP-REAL ((n + 1) + 1))) = p by RLVECT_1:13;
hence x in the carrier of (Tunit_circle ((n + 1) + 1)) by A23, A22, A17; :: thesis: verum
end;
then reconsider S1 = s1, S2 = s2 as Subset of (Tunit_circle ((n + 1) + 1)) 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. (TOP-REAL ((n + 1) + 1))),1) c= S1 \/ S2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) or x in S1 \/ S2 )
assume A27: x in Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) ; :: thesis: x in S1 \/ S2
then reconsider p = x as Point of (TOP-REAL ((n + 1) + 1)) ;
A28: ( p . ((n + 1) + 1) >= 0 or p . ((n + 1) + 1) <= 0 ) ;
|.p.| = 1 by A27, TOPREAL9:12;
then ( p in Sp or p in Sn ) by A28;
hence x in S1 \/ S2 by XBOOLE_0:def 3; :: thesis: verum
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),((Tunit_circle ((n + 1) + 1)) | (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),((Tunit_circle ((n + 1) + 1)) | (f .: A1)) by A12, A7, JORDAN24:12;
A36: f1 is continuous by A35, A12, A10, JORDAN24:13;
A37: rng f1 c= the carrier of ((Tunit_circle ((n + 1) + 1)) | (f .: A1)) ;
A38: [#] ((Tunit_circle ((n + 1) + 1)) | (f .: A1)) = f .: A1 by PRE_TOPC:def 5;
then A39: rng f1 c= the carrier of (Tunit_circle ((n + 1) + 1)) 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),((Tunit_circle ((n + 1) + 1)) | (f .: A2)) by A12, A7, JORDAN24:12;
A41: f2 is continuous by A40, A12, A10, JORDAN24:13;
A42: [#] ((Tunit_circle ((n + 1) + 1)) | (f .: A2)) = f .: A2 by PRE_TOPC:def 5;
then A43: rng f2 c= the carrier of (Tunit_circle ((n + 1) + 1)) 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 = f1 as Function of (TM | A1),(Tunit_circle ((n + 1) + 1)) by A39, FUNCT_2:2, A44;
A45: rng f2 c= the carrier of ((Tunit_circle ((n + 1) + 1)) | (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 = f2 as Function of (TM | A2),(Tunit_circle ((n + 1) + 1)) 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 being 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)) <= (n + 1) - 1 by A31, TOPDIM_2:24, A5, A6, A26, A48;
set TX = TM | (X1 /\ X2);
A55: [#] (TM | (X1 /\ X2)) = X1 /\ X2 by PRE_TOPC:def 5;
then reconsider TXA12 = A1 /\ A2 as Subset of (TM | (X1 /\ X2)) 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. (TOP-REAL (n + 1))),1);
deffunc H1( Nat) -> Element of K10(K11( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)) = PROJ (((n + 1) + 1),$1);
consider FF being FinSequence such that
A57: ( len FF = n + 1 & ( for k being Nat st k in dom FF holds
FF . k = H1(k) ) ) from FINSEQ_1:sch 2();
A58: rng FF c= Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng FF or x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) )
assume x in rng FF ; :: thesis: x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)
then consider i being object such that
A59: i in dom FF and
A60: FF . i = x by FUNCT_1:def 3;
reconsider i = i as Nat by A59;
H1(i) in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by FUNCT_2:8;
hence x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by A57, A59, A60; :: thesis: verum
end;
A61: Ball ((0. (TOP-REAL (n + 1))),1) c= Int (cl_Ball ((0. (TOP-REAL (n + 1))),1)) by TOPREAL9:16, TOPS_1:24;
then A62: ( cl_Ball ((0. (TOP-REAL (n + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n + 1))),1) is boundary & cl_Ball ((0. (TOP-REAL (n + 1))),1) is convex ) ;
reconsider FF = FF as FinSequence of Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by A58, FINSEQ_1:def 4;
reconsider FF = FF as Element of (n + 1) -tuples_on (Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)) by A57, FINSEQ_2:92;
set FFF = <:FF:>;
A63: s1 /\ s2 c= s2 by XBOOLE_1:17;
A64: <:FF:> .: s2 = cl_Ball ((0. (TOP-REAL (n + 1))),1) by A57, Th1, A15;
then A65: not s2 is empty ;
A66: dom <:FF:> = the carrier of (TOP-REAL ((n + 1) + 1)) by FUNCT_2:def 1;
then s1 /\ (dom <:FF:>) = s1 by XBOOLE_1:28;
then A67: dom (<:FF:> | s1) = s1 by RELAT_1:61;
s2 /\ (dom <:FF:>) = s2 by XBOOLE_1:28, A66;
then A68: dom (<:FF:> | s2) = s2 by RELAT_1:61;
A69: the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) = cl_Ball ((0. (TOP-REAL (n + 1))),1) by BROUWER:3;
then rng (<:FF:> | s2) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by RELAT_1:115, A64;
then reconsider Fs2 = <:FF:> | s2 as Function of ((TOP-REAL ((n + 1) + 1)) | s2),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:2, A16, A68;
A70: [#] ((TOP-REAL ((n + 1) + 1)) | s1) = s1 by PRE_TOPC:def 5;
Fs2 is being_homeomorphism by A57, Th1, A15;
then A71: s2, cl_Ball ((0. (TOP-REAL (n + 1))),1) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;
A72: <:FF:> .: s1 = cl_Ball ((0. (TOP-REAL (n + 1))),1) by A57, Th1, A14;
then A73: not s1 is empty ;
rng (<:FF:> | s1) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by RELAT_1:115, A72, A69;
then reconsider Fs1 = <:FF:> | s1 as Function of ((TOP-REAL ((n + 1) + 1)) | s1),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A67, FUNCT_2:2, A70;
A74: Fs1 .: (s1 /\ s2) c= <:FF:> .: (s1 /\ s2) by RELAT_1:128;
A75: Fs1 is being_homeomorphism by A57, Th1, A14;
then A76: rng Fs1 = [#] (Tdisk ((0. (TOP-REAL (n + 1))),1)) 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;
[#] ((Tunit_circle ((n + 1) + 1)) | (f .: TFA12)) = f .: TFA12 by PRE_TOPC:def 5;
then A80: rng fa c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s1) by A79, A70;
then reconsider fa = fa as Function of ((TM | F) | TFA12),(Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1, A70, A34, FUNCT_2:2;
A81: fa is continuous by A33, PRE_TOPC:26;
rng fa c= the carrier of (TOP-REAL ((n + 1) + 1)) by A17, XBOOLE_1:1;
then reconsider fa = fa as Function of ((TM | F) | TFA12),(TOP-REAL ((n + 1) + 1)) 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: <:FF:> .: (s1 /\ s2) = Sphere ((0. (TOP-REAL (n + 1))),1) by A57, Th1;
then Fs1 .: (s1 /\ s2) = Sphere ((0. (TOP-REAL (n + 1))),1) by XBOOLE_1:17, RELAT_1:129;
then A85: (Fs1 ") .: (Sphere ((0. (TOP-REAL (n + 1))),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 = (TM | (X1 /\ X2)) | TXA12 by PRE_TOPC:7, A50, A51, XBOOLE_1:27;
then reconsider fa = fa as Function of ((TM | (X1 /\ X2)) | TXA12),((TOP-REAL ((n + 1) + 1)) | s1) by A34, FUNCT_2:2, A80;
reconsider Ffa = Fs1 * fa as Function of ((TM | (X1 /\ X2)) | TXA12),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A73;
A88: [#] ((TM | (X1 /\ X2)) | 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. (TOP-REAL (n + 1))),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 = Ffa as Function of ((TM | (X1 /\ X2)) | TXA12),(TOP-REAL (n + 1)) by A91, XBOOLE_1:1, FUNCT_2:2, A89, A88;
Tunit_circle (n + 1) = Tcircle ((0. (TOP-REAL (n + 1))),1) by TOPREALB:def 7;
then A93: the carrier of (Tunit_circle (n + 1)) = Sphere ((0. (TOP-REAL (n + 1))),1) by TOPREALB:9;
then reconsider H = Ffa as Function of ((TM | (X1 /\ X2)) | TXA12),(Tunit_circle (n + 1)) by FUNCT_2:2, A89, A88, A90, A74, XBOOLE_1:1, A84;
Ffa is continuous by A92, PRE_TOPC:26;
then reconsider H = H as continuous Function of ((TM | (X1 /\ X2)) | TXA12),(Tunit_circle (n + 1)) by PRE_TOPC:27;
TXA12 is closed by A26, A48, TSEP_1:8;
then consider g being Function of (TM | (X1 /\ X2)),(Tunit_circle (n + 1)) such that
A94: g is continuous and
A95: g | TXA12 = H by A5, A56, A4;
A96: rng g c= the carrier of (TOP-REAL (n + 1)) by A93, XBOOLE_1:1;
A97: dom g = the carrier of (TM | (X1 /\ X2)) by FUNCT_2:def 1;
A98: rng g c= the carrier of (Tunit_circle (n + 1)) ;
reconsider g = g as Function of (TM | (X1 /\ X2)),(TOP-REAL (n + 1)) by A97, A96, FUNCT_2:2;
A99: g is continuous by A94, PRE_TOPC:26;
the carrier of (Tunit_circle (n + 1)) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by A93, A69, TOPREAL9:17;
then reconsider g = g as Function of (TM | (X1 /\ X2)),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A98, XBOOLE_1:1, FUNCT_2:2, A97;
reconsider G = (Fs1 ") * g as Function of (TM | (X1 /\ X2)),((TOP-REAL ((n + 1) + 1)) | s1) ;
A100: dom G = the carrier of (TM | (X1 /\ X2)) 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 = G as Function of (TM | (X1 /\ X2)),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A100;
A103: G is continuous by PRE_TOPC:26, A101;
reconsider G = G as Function of (TM | (X1 /\ X2)),(Tunit_circle ((n + 1) + 1)) 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 :: thesis: for xx being object st xx in (dom f1) /\ (dom G) holds
G . xx = f1 . xx
let xx be object ; :: thesis: ( xx in (dom f1) /\ (dom G) implies G . xx = f1 . xx )
assume A108: xx in (dom f1) /\ (dom G) ; :: thesis: G . xx = f1 . xx
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 ;
:: thesis: verum
end;
A111: now :: thesis: for xx being object st xx in (dom f2) /\ (dom G) holds
G . xx = f2 . xx
let xx be object ; :: thesis: ( xx in (dom f2) /\ (dom G) implies G . xx = f2 . xx )
assume A112: xx in (dom f2) /\ (dom G) ; :: thesis: G . xx = f2 . xx
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 ;
:: thesis: verum
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 | (A2 \/ (X1 /\ X2))),(Tunit_circle ((n + 1) + 1)) by A111, PARTFUN1:def 4, A104, A48, TOPGEN_5:10;
A116: dom f2G = the carrier of (TM | (A2 \/ (X1 /\ X2))) 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 = f2G as Function of (TM | (A2 \/ (X1 /\ X2))),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A116;
A118: f2G is continuous by PRE_TOPC:26;
reconsider f2G = f2G as Function of (TM | (A2 \/ (X1 /\ X2))),((TOP-REAL ((n + 1) + 1)) | s2) by FUNCT_2:2, A116, A115, A117, XBOOLE_1:1, A16;
( cl_Ball ((0. (TOP-REAL (n + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n + 1))),1) is boundary & cl_Ball ((0. (TOP-REAL (n + 1))),1) is convex ) by A61;
then consider H2 being Function of TM,((TOP-REAL ((n + 1) + 1)) | s2) such that
A119: H2 is continuous and
A120: H2 | (A2 \/ (X1 /\ X2)) = f2G by A118, PRE_TOPC:27, A71, TIETZE_2:24, A48;
A121: not TM is empty by A12;
then reconsider H2X = H2 | X2 as Function of (TM | X2),(((TOP-REAL ((n + 1) + 1)) | 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 | (A1 \/ (X1 /\ X2))),(Tunit_circle ((n + 1) + 1)) by A107, PARTFUN1:def 4, A104, A26, TOPGEN_5:10;
A125: dom f1G = the carrier of (TM | (A1 \/ (X1 /\ X2))) 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 = f1G as Function of (TM | (A1 \/ (X1 /\ X2))),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A125;
A128: f1G is continuous by PRE_TOPC:26;
reconsider f1G = f1G as Function of (TM | (A1 \/ (X1 /\ X2))),((TOP-REAL ((n + 1) + 1)) | s1) by FUNCT_2:2, A125, A126, A127, XBOOLE_1:1, A70;
s1, cl_Ball ((0. (TOP-REAL (n + 1))),1) are_homeomorphic by T_0TOPSP:def 1, A75, METRIZTS:def 1;
then consider H1 being Function of TM,((TOP-REAL ((n + 1) + 1)) | s1) such that
A129: H1 is continuous and
A130: H1 | (A1 \/ (X1 /\ X2)) = f1G by A62, A26, A128, PRE_TOPC:27, TIETZE_2:24;
reconsider H1X = H1 | X1 as Function of (TM | X1),(((TOP-REAL ((n + 1) + 1)) | s1) | (H1 .: X1)) by A121, JORDAN24:12, A73;
A131: H1X is continuous by JORDAN24:13, A73, A121, A129;
[#] (((TOP-REAL ((n + 1) + 1)) | s1) | (H1 .: X1)) = H1 .: X1 by PRE_TOPC:def 5;
then A132: rng H1X c= the carrier of ((TOP-REAL ((n + 1) + 1)) | 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 = H1X as Function of (TM | X1),((TOP-REAL ((n + 1) + 1)) | s1) by A132, FUNCT_2:2;
A136: H1X is continuous by A131, PRE_TOPC:26;
A137: rng H1X c= s1 by A70;
[#] (((TOP-REAL ((n + 1) + 1)) | s2) | (H2 .: X2)) = H2 .: X2 by PRE_TOPC:def 5;
then rng H2X c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s2) by XBOOLE_1:1;
then reconsider H2X = H2X as Function of (TM | X2),((TOP-REAL ((n + 1) + 1)) | s2) by A124, FUNCT_2:2;
A138: H2X is continuous by A122, PRE_TOPC:26;
reconsider H1X = H1X as Function of (TM | X1),(TOP-REAL ((n + 1) + 1)) by A137, XBOOLE_1:1, A135, FUNCT_2:2;
A139: rng H2X c= s2 by A16;
then reconsider H2X = H2X as Function of (TM | X2),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, A124, FUNCT_2:2;
A140: H2X is continuous by A138, PRE_TOPC:26;
A141: now :: thesis: for xx being object st xx in (dom H1X) /\ (dom H2X) holds
H1X . xx = H2X . xx
let xx be object ; :: thesis: ( xx in (dom H1X) /\ (dom H2X) implies H1X . xx = H2X . xx )
assume A142: xx in (dom H1X) /\ (dom H2X) ; :: thesis: H1X . xx = H2X . xx
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 A2 \/ (X1 /\ X2) by XBOOLE_0:def 3;
xx in A1 \/ (X1 /\ X2) by A145, XBOOLE_0:def 3;
then A147: H1 . xx = (H1 | (A1 \/ (X1 /\ X2))) . 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; :: thesis: verum
end;
H1X is continuous by A136, PRE_TOPC:26;
then reconsider H12 = H1X +* H2X as continuous Function of (TM | (X1 \/ X2)),(TOP-REAL ((n + 1) + 1)) by A140, A141, PARTFUN1:def 4, TOPGEN_5:10;
A149: TM | (X1 \/ X2) = TopStruct(# the carrier of TM, the topology of TM #) by A49, TSEP_1:93;
then reconsider H12 = H12 as Function of TM,(TOP-REAL ((n + 1) + 1)) ;
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. (TOP-REAL ((n + 1) + 1))),1) by A18, A21, A17, XBOOLE_1:8;
then reconsider H12 = H12 as Function of TM,(Tunit_circle ((n + 1) + 1)) by A155, XBOOLE_1:1, A17, A156, FUNCT_2:2;
take H12 ; :: thesis: ( H12 is continuous & H12 | F = f )
thus H12 is continuous by PRE_TOPC:27, A157; :: thesis: H12 | F = f
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 ; :: thesis: verum
end;
end;
end;
let f be continuous Function of (TM | F),(Tunit_circle (n + 1)); :: thesis: ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f
A160: S1[ 0 ]
proof
reconsider Z = 0 as Real ;
set TR = TOP-REAL 1;
set U = Tunit_circle (0 + 1);
let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= 0 holds
for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st
( g is continuous & g | F = f ) )
assume A161: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= 0 holds
for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st
( g is continuous & g | F = f )
let F be closed Subset of TM; :: thesis: ( ind (F `) <= 0 implies for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st
( g is continuous & g | F = f ) )
assume A162: ind (F `) <= 0 ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st
( g is continuous & g | F = f )
let f be continuous Function of (TM | F),(Tunit_circle (0 + 1)); :: thesis: ex g being Function of TM,(Tunit_circle (0 + 1)) st
( g is continuous & g | F = f )
A164: f " (rng f) = f " the carrier of (Tunit_circle (0 + 1)) by RELAT_1:143, RELAT_1:135;
Tunit_circle (0 + 1) = Tcircle ((0. (TOP-REAL 1)),1) by TOPREALB:def 7;
then A165: the carrier of (Tunit_circle (0 + 1)) = Sphere ((0. (TOP-REAL 1)),1) by TOPREALB:9;
0. (TOP-REAL 1) = 0* (0 + 1) by EUCLID:70
.= <*0*> by FINSEQ_2:59 ;
then A166: {<*(Z - 1)*>,<*(Z + 1)*>} = Fr (Ball ((0. (TOP-REAL 1)),1)) by TOPDIM_2:18;
A167: Fr (Ball ((0. (TOP-REAL 1)),1)) = Sphere ((0. (TOP-REAL 1)),1) by JORDAN:24;
then reconsider mONE = <*(- 1)*>, ONE = <*1*> as Point of (Tunit_circle (0 + 1)) by A165, TARSKI:def 2, A166;
reconsider Q = {ONE}, Q1 = {mONE} as closed Subset of (Tunit_circle (0 + 1)) ;
set F1 = f " Q;
set F2 = f " Q1;
A168: [#] (TM | F) = F by PRE_TOPC:def 5;
then reconsider A1 = f " Q, A2 = f " Q1 as Subset of TM by XBOOLE_1:1;
A169: dom f = F by A168, FUNCT_2:def 1;
Q \/ Q1 = the carrier of (Tunit_circle (0 + 1)) by A166, A167, A165, ENUMSET1:1;
then A170: (f " Q) \/ (f " Q1) = f " the carrier of (Tunit_circle (0 + 1)) by RELAT_1:140
.= F by A164, RELAT_1:134, A169 ;
f " Q1 is closed by PRE_TOPC:def 6;
then A171: A2 is closed by TSEP_1:8, A168;
f " Q is closed by PRE_TOPC:def 6;
then A172: A1 is closed by TSEP_1:8, A168;
ONE <> mONE
proof
assume ONE = mONE ; :: thesis: contradiction
then <*1*> . 1 = - 1 by FINSEQ_1:40;
hence contradiction ; :: thesis: verum
end;
then W: f " Q misses f " Q1 by ZFMISC_1:11, FUNCT_1:71;
TM | (F `) is second-countable by A161;
then consider X1, X2 being 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 - 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;
set h2 = (TM | X2) --> mONE;
A179: [#] (TM | X1) = X1 by PRE_TOPC:def 5;
A180: dom ((TM | X2) --> mONE) = the carrier of (TM | X2) ;
A181: [#] (TM | X2) = X2 by PRE_TOPC:def 5;
dom ((TM | X1) --> ONE) = the carrier of (TM | X1) ;
then (TM | X1) --> ONE tolerates (TM | X2) --> mONE by A178, A179, A180, A181, XBOOLE_0:def 7, PARTFUN1:56;
then reconsider h12 = ((TM | X1) --> ONE) +* ((TM | X2) --> mONE) as continuous Function of (TM | ([#] TM)),(Tunit_circle (0 + 1)) by A174, TOPGEN_5:10;
[#] (TM | ([#] TM)) = [#] TM by PRE_TOPC:def 5;
then reconsider H12 = h12 as Function of TM,(Tunit_circle (0 + 1)) ;
A182: for x being object st x in F holds
(H12 | F) . x = f . x
proof
let x be object ; :: thesis: ( x in F implies (H12 | F) . x = f . x )
assume A183: x in F ; :: thesis: (H12 | F) . x = f . x
then A184: (H12 | F) . x = h12 . x by FUNCT_1:49;
per cases ( x in f " Q or x in f " Q1 ) by A183, A170, XBOOLE_0:def 3;
suppose A185: x in f " Q ; :: thesis: (H12 | F) . x = f . x
then not x in dom ((TM | X2) --> mONE) by A175, A178, XBOOLE_0:def 4, A181;
then A186: H12 . x = ((TM | X1) --> ONE) . x by FUNCT_4:11;
A187: f . x in {ONE} by A185, FUNCT_1:def 7;
((TM | X1) --> ONE) . x = ONE by A185, A175, A179, FUNCOP_1:7;
hence (H12 | F) . x = f . x by A187, TARSKI:def 1, A186, A184; :: thesis: verum
end;
suppose A188: x in f " Q1 ; :: thesis: (H12 | F) . x = f . x
then A189: f . x in {mONE} by FUNCT_1:def 7;
A190: ((TM | X2) --> mONE) . x = mONE by A188, A176, A181, FUNCOP_1:7;
H12 . x = ((TM | X2) --> mONE) . x by A188, A176, A180, A181, FUNCT_4:13;
hence (H12 | F) . x = f . x by A189, TARSKI:def 1, A190, A184; :: thesis: verum
end;
end;
end;
take H12 ; :: thesis: ( H12 is continuous & H12 | F = f )
TM | ([#] TM) = TopStruct(# the carrier of TM, the topology of TM #) by TSEP_1:93;
hence H12 is continuous by PRE_TOPC:32; :: thesis: H12 | F = f
dom H12 = the carrier of TM by FUNCT_2:def 1;
then dom (H12 | F) = F by RELAT_1:62;
hence H12 | F = f by A182, A168, FUNCT_2:def 1; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A160, A3);
 then ex g being Function of TM,(Tunit_circle (n + 1)) st
( g is continuous & g | F = f ) by A1, A2;
hence ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f ; :: thesis: verum