let T be non empty TopSpace; :: thesis: ( T is T_4 implies T is Tychonoff )
assume A7:
T is T_4
; :: thesis: T is Tychonoff
let A be closed Subset of T; :: according to TOPGEN_5:def 4 :: thesis: for a being Point of T st a in A ` holds
ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} )
let a be Point of T; :: thesis: ( a in A ` implies ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) )
the carrier of (Closed-Interval-TSpace (- 1),1) = [.(- 1),1.]
by TOPMETR:25;
then reconsider j = 1, k = - 1 as Point of (Closed-Interval-TSpace (- 1),1) by XXREAL_1:1;
reconsider z = 0 , o = 1 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
:: thesis: ( a in A ` implies ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) )then reconsider aa =
{a},
A' =
A as non
empty closed Subset of
T by A7, URYSOHN1:27;
reconsider B =
A' \/ aa as
closed Subset of
T by TOPS_1:36;
set h =
((T | A') --> j) +* ((T | aa) --> k);
A9:
( the
carrier of
(T | A') = A & the
carrier of
(T | aa) = aa )
by PRE_TOPC:29;
A10:
(
(T | A') --> j = A' --> 1 &
(T | aa) --> k = aa --> k &
(A' --> 1) .: A c= {1} )
by FUNCOP_1:96, PRE_TOPC:29;
assume
a in A `
;
:: thesis: ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} )then
(
rng ((T | A') --> j) c= {1} &
rng ((T | aa) --> k) c= {k} &
{j} misses {k} & not
a in A )
by FUNCOP_1:19, XBOOLE_0:def 5, ZFMISC_1:17;
then A11:
(
A' misses aa &
rng ((T | A') --> j) misses rng ((T | aa) --> k) )
by XBOOLE_1:64, ZFMISC_1:56;
then reconsider h =
((T | A') --> j) +* ((T | aa) --> k) as
continuous Function of
(T | B),
(Closed-Interval-TSpace (- 1),1) by Th15;
A12:
h .: A c= {1}
by A10, A11, BOOLMARK:3;
A13:
(
dom ((T | aa) --> k) = aa &
a in aa )
by A9, FUNCOP_1:19, TARSKI:def 1;
then A14:
h . a =
((T | aa) --> k) . a
by FUNCT_4:14
.=
- 1
by A13, FUNCOP_1:13
;
A15:
(
a in B &
A c= B )
by A13, XBOOLE_0:def 3, XBOOLE_1:7;
consider g being
continuous Function of
T,
(Closed-Interval-TSpace (- 1),1) such that A16:
g | B = h
by A7, TIETZE:25;
consider p being
Function of
I[01] ,
(Closed-Interval-TSpace (- 1),1) such that A17:
(
p is
being_homeomorphism & ( for
r being
Real st
r in [.0 ,1.] holds
p . r = (2 * r) - 1 ) &
p . 0 = - 1 &
p . 1
= 1 )
by JGRAPH_5:42;
reconsider p' =
p /" as
continuous Function of
(Closed-Interval-TSpace (- 1),1),
I[01] by A17, TOPS_2:def 5;
reconsider f =
p' * g as
continuous Function of
T,
I[01] ;
take
f
;
:: thesis: ( f . a = 0 & f .: A c= {1} )
(
rng p = [#] (Closed-Interval-TSpace (- 1),1) &
p is
one-to-one )
by A17, TOPS_2:def 5;
then A19:
p' = p "
by TOPS_2:def 4;
then A20:
p' . k = z
by A17, FUNCT_2:32;
thus f . a =
p' . (g . a)
by FUNCT_2:21
.=
0
by A14, A15, A16, A20, FUNCT_1:72
;
:: thesis: f .: A c= {1}f .: A =
p' .: (g .: A)
by RELAT_1:159
.=
p' .: (h .: A)
by A15, A16, RELAT_1:162
;
then A21:
f .: A c= Im p',1
by A12, RELAT_1:156;
p' . j = o
by A17, A19, FUNCT_2:32;
hence
f .: A c= {1}
by A21, SETWISEO:13;
:: thesis: verum end;