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 that
A2: x in V and
A3: V in B ; :: thesis: ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V `) c= {1} )
A4: (V `) ` = V ;
V is open by A3, TOPS_2:def 1;
hence ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V `) c= {1} ) by A4, A1, A2; :: thesis: verum