let T be non empty TopSpace; :: thesis: for n being Nat st n >= 1 & ( for S being TopSpace
for A being non empty closed Subset of T
for B being Subset of S st ex X being Subset of (TOP-REAL n) st
( X is compact & not X is boundary & X is convex & B,X are_homeomorphic ) holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) ) holds
T is normal
let n be Nat; :: thesis: ( n >= 1 & ( for S being TopSpace
for A being non empty closed Subset of T
for B being Subset of S st ex X being Subset of (TOP-REAL n) st
( X is compact & not X is boundary & X is convex & B,X are_homeomorphic ) holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) ) implies T is normal )
set TR = TOP-REAL n;
assume that
A1: n >= 1 and
A2: for S being TopSpace
for A being non empty closed Subset of T
for B being Subset of S st ex X being Subset of (TOP-REAL n) st
( X is compact & not X is boundary & X is convex & B,X are_homeomorphic ) holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) ; :: thesis: T is normal
set CC = Closed-Interval-TSpace ((- 1),1);
for A being non empty closed Subset of T
for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
proof
let A be non empty closed Subset of T; :: thesis: for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
let f be continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)); :: thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
A3: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18;
A4: rng f c= REAL ;
dom f = the carrier of (T | A) by FUNCT_2:def 1;
then reconsider F = f as Function of (T | A),R^1 by A4, TOPMETR:17, FUNCT_2:2;
reconsider F = F as continuous Function of (T | A),R^1 by PRE_TOPC:26;
set IF1 = incl (F,n);
set n1 = n |-> 1;
set CH = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1));
A5: dom (incl (F,n)) = the carrier of (T | A) by FUNCT_2:def 1;
A6: [#] ((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by PRE_TOPC:def 5;
0. (TOP-REAL n) = 0* n by EUCLID:70;
then A7: 0. (TOP-REAL n) = n |-> 0 by EUCLID:def 4;
A8: rng (incl (F,n)) c= ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (incl (F,n)) or y in ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) )
assume A9: y in rng (incl (F,n)) ; :: thesis: y in ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))
then reconsider y = y as Point of (TOP-REAL n) ;
consider x being object such that
A10: ( x in dom (incl (F,n)) & (incl (F,n)) . x = y ) by A9, FUNCT_1:def 3;
reconsider x = x as Point of (T | A) by A10;
now :: thesis: for i being Nat st i in Seg n holds
y . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).]
let i be Nat; :: thesis: ( i in Seg n implies y . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).] )
assume A11: i in Seg n ; :: thesis: y . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).]
then A12: y . i = f . x by A10, TOPREALC:47;
A13: (0. (TOP-REAL n)) . i = 0 by A7;
(n |-> 1) . i = 1 by A11, FINSEQ_2:57;
hence y . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).] by A3, A13, A12; :: thesis: verum
end;
hence y in ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by Def2; :: thesis: verum
end;
then reconsider IF = incl (F,n) as Function of (T | A),((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) by A6, A5, FUNCT_2:2;
A14: IF is continuous by PRE_TOPC:27;
A15: n in Seg n by A1, FINSEQ_1:1;
consider g being Function of T,((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) such that
A16: ( g is continuous & g | A = IF ) by A2, A14, METRIZTS:def 1;
set P = PROJ (n,n);
A17: (PROJ (n,n)) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) = (PROJ (n,n)) | ((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) by A6, TMAP_1:def 4;
reconsider Pch = (PROJ (n,n)) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) as Function of ((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))),R^1 by PRE_TOPC:9;
reconsider Pg = Pch * g as Function of T,R^1 ;
A18: PROJ (n,n) is continuous by A15, TOPREALC:57;
A19: dom Pg = the carrier of T by FUNCT_2:def 1;
A20: rng Pg c= rng Pch by RELAT_1:26;
A21: (0. (TOP-REAL n)) . n = 0 by A7;
A22: (n |-> 1) . n = 1 by A1, FINSEQ_1:1, FINSEQ_2:57;
(PROJ (n,n)) .: (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) = [.(((0. (TOP-REAL n)) . n) - ((n |-> 1) . n)),(((0. (TOP-REAL n)) . n) + ((n |-> 1) . n)).] by A1, FINSEQ_1:1, Th7;
then rng Pg c= [.(- 1),1.] by RELAT_1:115, A20, A21, A22;
then reconsider Pg = Pg as Function of T,(Closed-Interval-TSpace ((- 1),1)) by A19, A3, FUNCT_2:2;
A23: Pg is continuous by A18, A17, A16, PRE_TOPC:27;
A24: dom Pch = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by FUNCT_2:def 1;
(Pch * g) | A = Pch * (g | A) by RELAT_1:83
.= (PROJ (n,n)) * IF by A16, A8, A24, RELAT_1:165
.= F by TOPREALC:56, A1 ;
hence ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f by A23; :: thesis: verum
end;
hence T is normal by TIETZE:24; :: thesis: verum