let T be non empty TopSpace; :: thesis: for x, y being Element of T st ( for W being open Subset of T st y in W holds
x in W ) holds
(0,1) --> (y,x) is continuous Function of Sierpinski_Space,T
let x, y be Element of T; :: thesis: ( ( for W being open Subset of T st y in W holds
x in W ) implies (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T )
assume A1: for W being open Subset of T st y in W holds
x in W ; :: thesis: (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T
A2: the carrier of Sierpinski_Space = {0,{0}} by WAYBEL18:def 9, CARD_1:49;
then reconsider i = (0,{0}) --> (y,x) as Function of Sierpinski_Space,T ;
A3: i . 1 = x by FUNCT_4:63, CARD_1:49;
A4: not 1 in {0} by TARSKI:def 1;
A5: 0 in {0} by TARSKI:def 1;
A6: 1 in {0,1} by TARSKI:def 2;
A7: i . 0 = y by FUNCT_4:63;
A8: now :: thesis: for W being Subset of T st W is open holds
i " W is open
let W be Subset of T; :: thesis: ( W is open implies i " W is open )
assume W is open ; :: thesis: i " W is open
then A9: ( ( y in W & x in W ) or ( not y in W & x in W ) or ( not y in W & not x in W ) ) by A1;
A10: ( i " W = {} or i " W = {0} or i " W = {1} or i " W = {0,1} ) by A2, ZFMISC_1:36, CARD_1:49;
i " W <> {0} by A7, A3, A6, A5, A4, A9, FUNCT_2:38, CARD_1:49;
then i " W in {{},{1},{0,1}} by ENUMSET1:def 1, A10;
then i " W in the topology of Sierpinski_Space by WAYBEL18:def 9;
hence i " W is open by PRE_TOPC:def 2; :: thesis: verum
end;
[#] T <> {} ;
hence (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T by A8, TOPS_2:43, CARD_1:49; :: thesis: verum