let T be non empty TopSpace; ( ( 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 ) implies T is normal )
assume A1:
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
; T is normal
for C, D being non empty closed Subset of T st C misses D holds
ex f being continuous Function of T,R^1 st
( f .: C = {0} & f .: D = {1} )
proof
set f2 =
T --> (R^1 1);
set f1 =
T --> (R^1 0);
let C,
D be non
empty closed Subset of
T;
( C misses D implies ex f being continuous Function of T,R^1 st
( f .: C = {0} & f .: D = {1} ) )
assume A2:
C misses D
;
ex f being continuous Function of T,R^1 st
( f .: C = {0} & f .: D = {1} )
set g1 =
(T --> (R^1 0)) | (T | C);
set g2 =
(T --> (R^1 1)) | (T | D);
set f =
((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D));
A3:
the
carrier of
(T | D) = D
by PRE_TOPC:8;
(T --> (R^1 1)) | (T | D) = (T --> (R^1 1)) | the
carrier of
(T | D)
by TMAP_1:def 4;
then A4:
rng ((T --> (R^1 1)) | (T | D)) c= rng (T --> (R^1 1))
by RELAT_1:70;
(T --> (R^1 0)) | (T | C) = (T --> (R^1 0)) | the
carrier of
(T | C)
by TMAP_1:def 4;
then
rng ((T --> (R^1 0)) | (T | C)) c= rng (T --> (R^1 0))
by RELAT_1:70;
then A5:
(rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D))) c= (rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1)))
by A4, XBOOLE_1:13;
A6:
T --> (R^1 0) = the
carrier of
T --> 0
by TOPREALB:def 2;
then A7:
rng (T --> (R^1 0)) = {0}
by FUNCOP_1:8;
A8:
T --> (R^1 1) = the
carrier of
T --> 1
by TOPREALB:def 2;
then A9:
rng (T --> (R^1 1)) = {1}
by FUNCOP_1:8;
A10:
the
carrier of
(T | C) = C
by PRE_TOPC:8;
then A11:
T | C misses T | D
by A2, A3, TSEP_1:def 3;
then
rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= (rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D)))
by Th13;
then A12:
rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= (rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1)))
by A5;
A13:
rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= [.(- 1),1.]
the
carrier of
(T | (C \/ D)) = C \/ D
by PRE_TOPC:8;
then A14:
T | (C \/ D) = (T | C) union (T | D)
by A10, A3, TSEP_1:def 2;
A15:
(T --> (R^1 1)) .: D = {1}
A18:
(T --> (R^1 0)) .: C = {0}
A21:
C \/ D is
closed
by TOPS_1:9;
the
carrier of
(Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.]
by TOPMETR:18;
then reconsider h =
((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) as
Function of
(T | (C \/ D)),
(Closed-Interval-TSpace ((- 1),1)) by A14, A13, FUNCT_2:6;
((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) is
continuous Function of
((T | C) union (T | D)),
R^1
by A11, TMAP_1:136;
then
h is
continuous
by A14, PRE_TOPC:27;
then consider g being
continuous Function of
T,
(Closed-Interval-TSpace ((- 1),1)) such that A22:
g | (C \/ D) = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))
by A1, A21;
reconsider F =
g as
continuous Function of
T,
R^1 by PRE_TOPC:26, TOPREALA:7;
take
F
;
( F .: C = {0} & F .: D = {1} )
thus F .: C =
(((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: C
by A22, FUNCT_2:97, XBOOLE_1:7
.=
((T --> (R^1 0)) | (T | C)) .: C
by A10, A11, Th14
.=
((T --> (R^1 0)) | C) .: C
by A10, TMAP_1:def 3
.=
{0}
by A18, RELAT_1:129
;
F .: D = {1}
thus F .: D =
(((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: D
by A22, FUNCT_2:97, XBOOLE_1:7
.=
((T --> (R^1 1)) | (T | D)) .: D
by A3, A11, Th14
.=
((T --> (R^1 1)) | D) .: D
by A3, TMAP_1:def 3
.=
{1}
by A15, RELAT_1:129
;
verum
end;
hence
T is normal
by Th18; verum