let X be T_1 TopSpace; :: thesis: ( X is Tychonoff implies for B being prebasis of X
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} ) )
assume A1: X is Tychonoff ; :: thesis: for B being prebasis of X
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} )
let B be prebasis of X; :: thesis: 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} )
let x be Point of X; :: thesis: 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} )
let V be Subset of X; :: thesis: ( x in V & V in B implies ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) )
assume A2: ( x in V & V in B ) ; :: thesis: ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} )
B is open by YELLOW_9:28;
then V is open by A2, TOPS_2:def 1;
then ( (V ` ) ` = V & V ` is closed ) ;
hence ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) by A1, A2, Def4; :: thesis: verum