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, Th89; :: 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
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 Th44;
A14: ( Y1 meets X1 union X2 implies Y1 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th44;
A15: now
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 Th11;
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 Th22;
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, Th37;
A22: now
A23: now
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, Th90;
then g | (Y2 meet (X1 union X2)) is_continuous_at x2 by Th49;
hence g is_continuous_at x by A7, A9, A10, A11, A13, A17, A18, A24, Th37, Th86; :: thesis: verum
end;
A25: now
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, Th90;
then g | (Y1 meet (X1 union X2)) is_continuous_at x1 by Th49;
hence g is_continuous_at x by A7, A9, A10, A11, A14, A17, A18, A26, Th37, Th86; :: 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, Th16; :: thesis: verum
end;
A28: now
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, Th15;
consider x1 being Point of X1 such that
A31: x1 = x00 by A7, Th17;
consider x2 being Point of X2 such that
A32: x2 = x00 by A7, Th17;
( g | X1 is_continuous_at x1 & g | X2 is_continuous_at x2 ) by A4, A5, Th49;
hence g is_continuous_at x by A29, A30, A31, A32, Th123; :: thesis: verum
end;
( Y1 union Y2 meets X1 union X2 & Z meets X1 union X2 ) by A7, A9, A10, A11, A16, A17, A18, Th38;
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, Th16; :: thesis: verum
end;
now
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, Th36;
A35: now
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, Th90;
then g | (Y2 meet (X1 union X2)) is_continuous_at x2 by Th49;
hence g is_continuous_at x by A9, A10, A11, A13, A33, A36, Th36, Th86; :: thesis: verum
end;
A37: now
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, Th90;
then g | (Y1 meet (X1 union X2)) is_continuous_at x1 by Th49;
hence g is_continuous_at x by A9, A10, A11, A14, A33, A38, Th36, Th86; :: thesis: verum
end;
Y1 is SubSpace of Y1 union Y2 by TSEP_1:22;
then Y1 union Y2 meets X1 union X2 by A34, Th23;
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, Th36;
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, Th16; :: thesis: verum
end;
hence g is_continuous_at x by A15; :: thesis: verum
end;
now
A40: now
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, Th49;
hence g is_continuous_at x by A41, Th88; :: thesis: verum
end;
A42: now
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, Th49;
hence g is_continuous_at x by A43, Th88; :: 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, Th35;
then A47: X2 is open SubSpace of X1 union X2 by A45, Th46;
A48: now
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, Th49;
hence g is_continuous_at x by A47, A49, Th86; :: thesis: verum
end;
Y1 misses X2 by A44, A45, A46, Th35;
then A50: X1 is open SubSpace of X1 union X2 by A44, Th46;
now
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, Th49;
hence g is_continuous_at x by A50, A51, Th86; :: thesis: verum
end;
hence g is_continuous_at x by A48, Th16; :: 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 Th49; :: thesis: verum
end;