let T be non empty TopSpace; :: thesis: for V being open Subset of T holds chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space
let V be open Subset of T; :: thesis: chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space
reconsider c = chi (V, the carrier of T) as Function of T,Sierpinski_Space by WAYBEL18:def 9;
A1: c " {0,1} = [#] T by FUNCT_2:40;
c = chi ((c " {1}), the carrier of T) by FUNCT_3:40;
then A2: V = c " {1} by FUNCT_3:38;
A3: c " {} = {} T ;
A4: now :: thesis: for W being Subset of Sierpinski_Space st W is open holds
c " W is open
let W be Subset of Sierpinski_Space; :: thesis: ( W is open implies c " W is open )
assume W is open ; :: thesis: c " W is open
then W in the topology of Sierpinski_Space by PRE_TOPC:def 2;
then W in {{},{1},{0,1}} by WAYBEL18:def 9;
hence c " W is open by A2, A3, A1, ENUMSET1:def 1; :: thesis: verum
end;
[#] Sierpinski_Space <> {} ;
hence chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space by A4, TOPS_2:43; :: thesis: verum