let T be non empty TopSpace; 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; ( 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 )
; 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;
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 = flet f be
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
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))
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;
verum
end;
hence
T is normal
by TIETZE:24; verum