let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds
for g being Function of (X1 union X2),Y holds
( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_weakly_separated implies for g being Function of (X1 union X2),Y holds
( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) ) )
assume A1: X1,X2 are_weakly_separated ; :: thesis: for g being Function of (X1 union X2),Y holds
( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )
let g be Function of (X1 union X2),Y; :: thesis: ( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )
A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;
A3: X1 is SubSpace of X1 union X2 by TSEP_1:22;
hence ( g is continuous Function of (X1 union X2),Y implies ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) ) by A2, Th82; :: thesis: ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y implies g is continuous Function of (X1 union X2),Y )
thus ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y implies g is continuous Function of (X1 union X2),Y ) :: thesis: verum
proof
assume that
A4: g | X1 is continuous Function of X1,Y and
A5: g | X2 is continuous Function of X2,Y ; :: thesis: g is continuous Function of (X1 union X2),Y
for x being Point of (X1 union X2) holds g is_continuous_at x
proof
set X0 = X1 union X2;
let x be Point of (X1 union X2); :: thesis: g is_continuous_at x
A6: ( X1 meets X2 implies g is_continuous_at x )
proof
assume A7: X1 meets X2 ; :: thesis: g is_continuous_at x
A8: now :: thesis: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies g is_continuous_at x )
assume A9: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis: g is_continuous_at x
then consider Y1, Y2 being non empty open SubSpace of X such that
A10: Y1 meet (X1 union X2) is SubSpace of X1 and
A11: Y2 meet (X1 union X2) is SubSpace of X2 and
A12: ( X1 union X2 is SubSpace of Y1 union Y2 or ex Z being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Z & Z meet (X1 union X2) is SubSpace of X1 meet X2 ) ) by A1, A7, TSEP_1:89;
A13: ( Y2 meets X1 union X2 implies Y2 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th39;
A14: ( Y1 meets X1 union X2 implies Y1 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th39;
A15: now :: thesis: ( X1 union X2 is not SubSpace of Y1 union Y2 implies g is_continuous_at x )
X is SubSpace of X by TSEP_1:2;
then reconsider X12 = TopStruct(# the carrier of X, the topology of X #) as SubSpace of X by Th6;
assume A16: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: g is_continuous_at x
then consider Z being non empty closed SubSpace of X such that
A17: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Z and
A18: Z meet (X1 union X2) is SubSpace of X1 meet X2 by A12;
the carrier of (X1 union X2) c= the carrier of X12 by BORSUK_1:1;
then A19: X1 union X2 is SubSpace of X12 by TSEP_1:4;
then X12 meets X1 union X2 by Th17;
then A20: ((Y1 union Y2) union Z) meet (X1 union X2) = TopStruct(# the carrier of (X1 union X2), the topology of (X1 union X2) #) by A17, A19, TSEP_1:28;
A21: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) by A7, A9, A10, A11, A17, A18, Th32;
A22: now :: thesis: ( ex x12 being Point of ((Y1 union Y2) meet (X1 union X2)) st x12 = x implies g is_continuous_at x )
A23: now :: thesis: ( ex x2 being Point of (Y2 meet (X1 union X2)) st x2 = x implies g is_continuous_at x )
given x2 being Point of (Y2 meet (X1 union X2)) such that A24: x2 = x ; :: thesis: g is_continuous_at x
g | (Y2 meet (X1 union X2)) is continuous by A2, A5, A11, Th83;
then g | (Y2 meet (X1 union X2)) is_continuous_at x2 ;
hence g is_continuous_at x by A7, A9, A10, A11, A13, A17, A18, A24, Th32, Th79; :: thesis: verum
end;
A25: now :: thesis: ( ex x1 being Point of (Y1 meet (X1 union X2)) st x1 = x implies g is_continuous_at x )
given x1 being Point of (Y1 meet (X1 union X2)) such that A26: x1 = x ; :: thesis: g is_continuous_at x
g | (Y1 meet (X1 union X2)) is continuous by A3, A4, A10, Th83;
then g | (Y1 meet (X1 union X2)) is_continuous_at x1 ;
hence g is_continuous_at x by A7, A9, A10, A11, A14, A17, A18, A26, Th32, Th79; :: thesis: verum
end;
assume A27: ex x12 being Point of ((Y1 union Y2) meet (X1 union X2)) st x12 = x ; :: thesis: g is_continuous_at x
(Y1 union Y2) meet (X1 union X2) = (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) by A21, TSEP_1:32;
hence g is_continuous_at x by A27, A25, A23, Th11; :: thesis: verum
end;
A28: now :: thesis: ( ex x0 being Point of (Z meet (X1 union X2)) st x0 = x implies g is_continuous_at x )
given x0 being Point of (Z meet (X1 union X2)) such that A29: x0 = x ; :: thesis: g is_continuous_at x
consider x00 being Point of (X1 meet X2) such that
A30: x00 = x0 by A18, Th10;
consider x1 being Point of X1 such that
A31: x1 = x00 by A7, Th12;
consider x2 being Point of X2 such that
A32: x2 = x00 by A7, Th12;
( g | X1 is_continuous_at x1 & g | X2 is_continuous_at x2 ) by A4, A5, Th44;
hence g is_continuous_at x by A29, A30, A31, A32, Th111; :: thesis: verum
end;
( Y1 union Y2 meets X1 union X2 & Z meets X1 union X2 ) by A7, A9, A10, A11, A16, A17, A18, Th33;
then ((Y1 union Y2) meet (X1 union X2)) union (Z meet (X1 union X2)) = TopStruct(# the carrier of (X1 union X2), the topology of (X1 union X2) #) by A20, TSEP_1:32;
hence g is_continuous_at x by A22, A28, Th11; :: thesis: verum
end;
now :: thesis: ( X1 union X2 is SubSpace of Y1 union Y2 implies g is_continuous_at x )
assume A33: X1 union X2 is SubSpace of Y1 union Y2 ; :: thesis: g is_continuous_at x
then A34: Y1 meets X1 union X2 by A9, A10, A11, Th31;
A35: now :: thesis: ( ex x2 being Point of (Y2 meet (X1 union X2)) st x2 = x implies g is_continuous_at x )
given x2 being Point of (Y2 meet (X1 union X2)) such that A36: x2 = x ; :: thesis: g is_continuous_at x
g | (Y2 meet (X1 union X2)) is continuous by A2, A5, A11, Th83;
then g | (Y2 meet (X1 union X2)) is_continuous_at x2 ;
hence g is_continuous_at x by A9, A10, A11, A13, A33, A36, Th31, Th79; :: thesis: verum
end;
A37: now :: thesis: ( ex x1 being Point of (Y1 meet (X1 union X2)) st x1 = x implies g is_continuous_at x )
given x1 being Point of (Y1 meet (X1 union X2)) such that A38: x1 = x ; :: thesis: g is_continuous_at x
g | (Y1 meet (X1 union X2)) is continuous by A3, A4, A10, Th83;
then g | (Y1 meet (X1 union X2)) is_continuous_at x1 ;
hence g is_continuous_at x by A9, A10, A11, A14, A33, A38, Th31, Th79; :: thesis: verum
end;
Y1 is SubSpace of Y1 union Y2 by TSEP_1:22;
then Y1 union Y2 meets X1 union X2 by A34, Th18;
then A39: (Y1 union Y2) meet (X1 union X2) = X1 union X2 by A33, TSEP_1:28;
Y2 meets X1 union X2 by A9, A10, A11, A33, Th31;
then (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) = X1 union X2 by A34, A39, TSEP_1:32;
hence g is_continuous_at x by A37, A35, Th11; :: thesis: verum
end;
hence g is_continuous_at x by A15; :: thesis: verum
end;
now :: thesis: ( ( X1 is SubSpace of X2 or X2 is SubSpace of X1 ) implies g is_continuous_at x )
A40: now :: thesis: ( X2 is SubSpace of X1 implies g is_continuous_at x )
assume X2 is SubSpace of X1 ; :: thesis: g is_continuous_at x
then A41: TopStruct(# the carrier of X1, the topology of X1 #) = X1 union X2 by TSEP_1:23;
then reconsider x1 = x as Point of X1 ;
g | X1 is_continuous_at x1 by A4, Th44;
hence g is_continuous_at x by A41, Th81; :: thesis: verum
end;
A42: now :: thesis: ( X1 is SubSpace of X2 implies g is_continuous_at x )
assume X1 is SubSpace of X2 ; :: thesis: g is_continuous_at x
then A43: TopStruct(# the carrier of X2, the topology of X2 #) = X1 union X2 by TSEP_1:23;
then reconsider x2 = x as Point of X2 ;
g | X2 is_continuous_at x2 by A5, Th44;
hence g is_continuous_at x by A43, Th81; :: thesis: verum
end;
assume ( X1 is SubSpace of X2 or X2 is SubSpace of X1 ) ; :: thesis: g is_continuous_at x
hence g is_continuous_at x by A42, A40; :: thesis: verum
end;
hence g is_continuous_at x by A8; :: thesis: verum
end;
( X1 misses X2 implies g is_continuous_at x )
proof
assume X1 misses X2 ; :: thesis: g is_continuous_at x
then X1,X2 are_separated by A1, TSEP_1:78;
then consider Y1, Y2 being non empty open SubSpace of X such that
A44: X1 is SubSpace of Y1 and
A45: X2 is SubSpace of Y2 and
A46: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) by TSEP_1:77;
Y2 misses X1 by A44, A45, A46, Th30;
then A47: X2 is open SubSpace of X1 union X2 by A45, Th41;
A48: now :: thesis: ( ex x2 being Point of X2 st x2 = x implies g is_continuous_at x )
given x2 being Point of X2 such that A49: x2 = x ; :: thesis: g is_continuous_at x
g | X2 is_continuous_at x2 by A5, Th44;
hence g is_continuous_at x by A47, A49, Th79; :: thesis: verum
end;
Y1 misses X2 by A44, A45, A46, Th30;
then A50: X1 is open SubSpace of X1 union X2 by A44, Th41;
now :: thesis: ( ex x1 being Point of X1 st x1 = x implies g is_continuous_at x )
given x1 being Point of X1 such that A51: x1 = x ; :: thesis: g is_continuous_at x
g | X1 is_continuous_at x1 by A4, Th44;
hence g is_continuous_at x by A50, A51, Th79; :: thesis: verum
end;
hence g is_continuous_at x by A48, Th11; :: thesis: verum
end;
hence g is_continuous_at x by A6; :: thesis: verum
end;
hence g is continuous Function of (X1 union X2),Y by Th44; :: thesis: verum
end;