let T be non empty TopSpace; :: thesis: ( ( 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
; :: thesis: 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
let C,
D be non
empty closed Subset of
T;
:: thesis: ( 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
;
:: thesis: ex f being continuous Function of T,R^1 st
( f .: C = {0 } & f .: D = {1} )
set f1 =
T --> (R^1 0 );
set f2 =
T --> (R^1 1);
set g1 =
(T --> (R^1 0 )) | (T | C);
set g2 =
(T --> (R^1 1)) | (T | D);
A3:
(
(T --> (R^1 0 )) | (T | C) is
continuous &
(T --> (R^1 1)) | (T | D) is
continuous )
by TMAP_1:68;
set f =
((T --> (R^1 0 )) | (T | C)) union ((T --> (R^1 1)) | (T | D));
A4:
( the
carrier of
(T | C) = C & the
carrier of
(T | D) = D )
by PRE_TOPC:29;
the
carrier of
(T | (C \/ D)) = C \/ D
by PRE_TOPC:29;
then A5:
T | (C \/ D) = (T | C) union (T | D)
by A4, TSEP_1:def 2;
A6:
the
carrier of
(Closed-Interval-TSpace (- 1),1) = [.(- 1),1.]
by TOPMETR:25;
A7:
T | C misses T | D
by A2, A4, TSEP_1:def 3;
then A8:
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 Th15;
(
(T --> (R^1 0 )) | (T | C) = (T --> (R^1 0 )) | the
carrier of
(T | C) &
(T --> (R^1 1)) | (T | D) = (T --> (R^1 1)) | the
carrier of
(T | D) )
by TMAP_1:def 3;
then
(
rng ((T --> (R^1 0 )) | (T | C)) c= rng (T --> (R^1 0 )) &
rng ((T --> (R^1 1)) | (T | D)) c= rng (T --> (R^1 1)) )
by RELAT_1:99;
then
(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 XBOOLE_1:13;
then A9:
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 A8, XBOOLE_1:1;
A10:
T --> (R^1 0 ) = the
carrier of
T --> 0
by TOPREALB:def 2;
then A11:
rng (T --> (R^1 0 )) = {0 }
by FUNCOP_1:14;
A12:
T --> (R^1 1) = the
carrier of
T --> 1
by TOPREALB:def 2;
then A13:
rng (T --> (R^1 1)) = {1}
by FUNCOP_1:14;
rng (((T --> (R^1 0 )) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= [.(- 1),1.]
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 A5, A6, FUNCT_2:8;
((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 A3, A7, TMAP_1:148;
then A14:
h is
continuous
by A5, PRE_TOPC:57;
C \/ D is
closed
by TOPS_1:36;
then consider g being
continuous Function of
T,
(Closed-Interval-TSpace (- 1),1) such that A15:
g | (C \/ D) = ((T --> (R^1 0 )) | (T | C)) union ((T --> (R^1 1)) | (T | D))
by A1, A14;
reconsider F =
g as
continuous Function of
T,
R^1 by PRE_TOPC:56, TOPREALA:28;
take
F
;
:: thesis: ( F .: C = {0 } & F .: D = {1} )
A16:
C c= C
;
A17:
(T --> (R^1 0 )) .: C = {0 }
thus F .: C =
(((T --> (R^1 0 )) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: C
by A15, FUNCT_2:174, XBOOLE_1:7
.=
((T --> (R^1 0 )) | (T | C)) .: C
by A4, A7, A16, Th16
.=
((T --> (R^1 0 )) | C) .: C
by A4, TMAP_1:def 3
.=
{0 }
by A17, RELAT_1:162
;
:: thesis: F .: D = {1}
A21:
D c= D
;
A22:
(T --> (R^1 1)) .: D = {1}
thus F .: D =
(((T --> (R^1 0 )) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: D
by A15, FUNCT_2:174, XBOOLE_1:7
.=
((T --> (R^1 1)) | (T | D)) .: D
by A4, A7, A21, Th16
.=
((T --> (R^1 1)) | D) .: D
by A4, TMAP_1:def 3
.=
{1}
by A22, RELAT_1:162
;
:: thesis: verum
end;
hence
T is normal
by Th20; :: thesis: verum