let S be non empty TopSpace; :: thesis: for T being non empty Hausdorff TopSpace
for f, g being continuous Function of S,T holds
( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds
X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds
X is closed ) )
let T be non empty Hausdorff TopSpace; :: thesis: for f, g being continuous Function of S,T holds
( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds
X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds
X is closed ) )
let f, g be continuous Function of S,T; :: thesis: ( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds
X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds
X is closed ) )
{ p where p is Point of S : f . p <> g . p } c= the carrier of S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of S : f . p <> g . p } or x in the carrier of S )
assume x in { p where p is Point of S : f . p <> g . p } ; :: thesis: x in the carrier of S
then ex a being Point of S st
( x = a & f . a <> g . a ) ;
hence x in the carrier of S ; :: thesis: verum
end;
then reconsider A = { p where p is Point of S : f . p <> g . p } as Subset of S ;
A1: [#] T <> {} ;
thus for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds
X is open :: thesis: for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds
X is closed
proof
let X be Subset of S; :: thesis: ( X = { p where p is Point of S : f . p <> g . p } implies X is open )
assume A2: X = { p where p is Point of S : f . p <> g . p } ; :: thesis: X is open
for x being set holds
( x in X iff ex Q being Subset of S st
( Q is open & Q c= X & x in Q ) )
proof
let x be set ; :: thesis: ( x in X iff ex Q being Subset of S st
( Q is open & Q c= X & x in Q ) )
hereby :: thesis: ( ex Q being Subset of S st
( Q is open & Q c= X & x in Q ) implies x in X )
assume x in X ; :: thesis: ex Q being Element of bool the carrier of S st
( Q is open & Q c= X & x in Q )
then consider p being Point of S such that
A3: x = p and
A4: f . p <> g . p by A2;
consider W, V being Subset of T such that
A5: ( W is open & V is open ) and
A6: f . p in W and
A7: g . p in V and
A8: W misses V by A4, PRE_TOPC:def 10;
dom g = the carrier of S by FUNCT_2:def 1;
then [x,(g . p)] in g by A3, FUNCT_1:def 2;
then A9: x in g " V by A7, RELAT_1:def 14;
take Q = (f " W) /\ (g " V); :: thesis: ( Q is open & Q c= X & x in Q )
( f " W is open & g " V is open ) by A1, A5, TOPS_2:43;
hence Q is open ; :: thesis: ( Q c= X & x in Q )
thus Q c= X :: thesis: x in Q
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Q or q in X )
assume A10: q in Q ; :: thesis: q in X
then q in f " W by XBOOLE_0:def 4;
then consider yf being object such that
A11: [q,yf] in f and
A12: yf in W by RELAT_1:def 14;
q in g " V by A10, XBOOLE_0:def 4;
then consider yg being object such that
A13: ( [q,yg] in g & yg in V ) by RELAT_1:def 14;
A14: ( yg = g . q & not yg in W ) by A8, A13, FUNCT_1:1, XBOOLE_0:3;
yf = f . q by A11, FUNCT_1:1;
hence q in X by A2, A10, A12, A14; :: thesis: verum
end;
dom f = the carrier of S by FUNCT_2:def 1;
then [x,(f . p)] in f by A3, FUNCT_1:def 2;
then x in f " W by A6, RELAT_1:def 14;
hence x in Q by A9, XBOOLE_0:def 4; :: thesis: verum
end;
given Q being Subset of S such that Q is open and
A15: ( Q c= X & x in Q ) ; :: thesis: x in X
thus x in X by A15; :: thesis: verum
end;
hence X is open by TOPS_1:25; :: thesis: verum
end;
then A16: A is open ;
let X be Subset of S; :: thesis: ( X = { p where p is Point of S : f . p = g . p } implies X is closed )
assume A17: X = { p where p is Point of S : f . p = g . p } ; :: thesis: X is closed
X ` = A
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= X `
let x be object ; :: thesis: ( x in X ` implies x in A )
assume A18: x in X ` ; :: thesis: x in A
then not x in X by XBOOLE_0:def 5;
then f . x <> g . x by A17, A18;
hence x in A by A18; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in X ` )
assume x in A ; :: thesis: x in X `
then consider p being Point of S such that
A19: x = p and
A20: f . p <> g . p ;
now :: thesis: not p in { t where t is Point of S : f . t = g . t }
assume p in { t where t is Point of S : f . t = g . t } ; :: thesis: contradiction
then ex t being Point of S st
( p = t & f . t = g . t ) ;
hence contradiction by A20; :: thesis: verum
end;
hence x in X ` by A17, A19, XBOOLE_0:def 5; :: thesis: verum
end;
hence X is closed by A16; :: thesis: verum