let X, Y be non empty TopSpace; 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; ( 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
; 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; ( 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; ( 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 )
verumproof
assume that A4:
g | X1 is
continuous Function of
X1,
Y
and A5:
g | X2 is
continuous Function of
X2,
Y
;
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);
g is_continuous_at x
A6:
(
X1 meets X2 implies
g is_continuous_at x )
proof
assume A7:
X1 meets X2
;
g is_continuous_at x
A8:
now ( 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 )
;
g is_continuous_at xthen 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 ( 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
;
g is_continuous_at xthen 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 ( ex x12 being Point of ((Y1 union Y2) meet (X1 union X2)) st x12 = x implies g is_continuous_at x )A23:
now ( 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
;
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;
verum end; A25:
now ( 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
;
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;
verum end; assume A27:
ex
x12 being
Point of
((Y1 union Y2) meet (X1 union X2)) st
x12 = x
;
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;
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;
verum end; now ( 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
;
g is_continuous_at xthen A34:
Y1 meets X1 union X2
by A9, A10, A11, Th31;
A35:
now ( 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
;
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;
verum end; A37:
now ( 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
;
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;
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;
verum end; hence
g is_continuous_at x
by A15;
verum end;
hence
g is_continuous_at x
by A8;
verum
end;
(
X1 misses X2 implies
g is_continuous_at x )
proof
assume
X1 misses X2
;
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;
Y1 misses X2
by A44, A45, A46, Th30;
then A50:
X1 is
open SubSpace of
X1 union X2
by A44, Th41;
hence
g is_continuous_at x
by A48, Th11;
verum
end;
hence
g is_continuous_at x
by A6;
verum
end;
hence
g is
continuous Function of
(X1 union X2),
Y
by Th44;
verum
end;