let X be non empty T_1 TopSpace; :: thesis: for B being prebasis of X st ( for x being Point of X
for V being Subset of X st x in V & V in B holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) ) holds
X is Tychonoff
let BB be prebasis of X; :: thesis: ( ( for x being Point of X
for V being Subset of X st x in V & V in BB holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) ) implies X is Tychonoff )
assume A1:
for x being Point of X
for V being Subset of X st x in V & V in BB holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} )
; :: thesis: X is Tychonoff
let A be closed Subset of X; :: according to TOPGEN_5:def 4 :: thesis: for a being Point of X st a in A ` holds
ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )
let a be Point of X; :: thesis: ( a in A ` implies ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} ) )
assume A2:
a in A `
; :: thesis: ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )
( A ` is open & FinMeetCl BB is Basis of X )
by YELLOW_9:23;
then consider B being Subset of X such that
A3:
( B in FinMeetCl BB & a in B & B c= A ` )
by A2, YELLOW_9:31;
consider F being Subset-Family of X such that
A4:
( F c= BB & F is finite & B = Intersect F )
by A3, CANTOR_1:def 4;
reconsider z = 0 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
per cases
( F is empty or not F is empty )
;
suppose
not
F is
empty
;
:: thesis: ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )then reconsider F =
F as non
empty finite Subset-Family of
X by A4;
defpred S1[
set ,
set ]
means ex
S being
Subset of
X ex
f being
continuous Function of
X,
I[01] st
(
S = $1 &
f = $2 &
f . a = 0 &
f .: (S ` ) c= {1} );
A5:
for
x being
set st
x in F holds
ex
y being
set st
S1[
x,
y]
consider G being
Function such that A8:
(
dom G = F & ( for
x being
set st
x in F holds
S1[
x,
G . x] ) )
from CLASSES1:sch 1(A5);
G is
Function-yielding
then reconsider G =
G as
ManySortedFunction of
by A8, PARTFUN1:def 4, RELAT_1:def 18;
then consider f being
continuous Function of
X,
I[01] such that A9:
for
x being
Point of
X for
S being non
empty finite Subset of
REAL st
S = rng ((commute G) . x) holds
f . x = max S
by Th55;
take
f
;
:: thesis: ( f . a = 0 & f .: A c= {1} )reconsider Sa =
{0 } as non
empty finite Subset of
REAL ;
consider z being
Element of
F;
set R =
I[01] ;
rng G c= Funcs the
carrier of
X,the
carrier of
I[01]
then
G is
Function of
F,
(Funcs the carrier of X,the carrier of I[01] )
by A8, FUNCT_2:4;
then A11:
G in Funcs F,
(Funcs the carrier of X,the carrier of I[01] )
by FUNCT_2:11;
then
commute G in Funcs the
carrier of
X,
(Funcs F,the carrier of I[01] )
by FUNCT_6:85;
then reconsider cG =
commute G as
Function of the
carrier of
X,
(Funcs F,the carrier of I[01] ) by FUNCT_2:121;
reconsider cGa =
cG . a as
Function of
F,the
carrier of
I[01] by FUNCT_2:121;
A12:
dom cGa = F
by FUNCT_2:def 1;
Sa = rng ((commute G) . a)
hence f . a =
max Sa
by A9
.=
0
by XXREAL_2:11
;
:: thesis: f .: A c= {1}let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in f .: A or z in {1} )assume
z in f .: A
;
:: thesis: z in {1}then consider x being
set such that A14:
(
x in dom f &
x in A &
z = f . x )
by FUNCT_1:def 12;
reconsider x =
x as
Element of
X by A14;
reconsider cGx =
cG . x as
Function of
F,the
carrier of
I[01] by FUNCT_2:121;
reconsider S =
rng cGx as non
empty finite Subset of
REAL by BORSUK_1:83, XBOOLE_1:1;
A15:
f . x = max S
by A9;
A16:
for
r being
ext-real number st
r in S holds
r <= 1
by BORSUK_1:83, XXREAL_1:1;
not
x in B
by A3, A14, XBOOLE_0:def 5;
then consider w being
set such that A18:
(
w in F & not
x in w )
by A4, SETFAM_1:58;
consider T being
Subset of
X,
g being
continuous Function of
X,
I[01] such that A19:
(
T = w &
g = G . w &
g . a = 0 &
g .: (T ` ) c= {1} )
by A8, A18;
x in T `
by A18, A19, SUBSET_1:50;
then
g . x in g .: (T ` )
by FUNCT_2:43;
then
g . x = 1
by A19, TARSKI:def 1;
then
(
w in dom cGx &
cGx . w = 1 )
by A11, A18, A19, FUNCT_6:86;
then
1
in S
by FUNCT_1:def 5;
then
max S = 1
by A16, XXREAL_2:def 8;
hence
z in {1}
by A14, A15, TARSKI:def 1;
:: thesis: verum end;