let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )
let X1, X2 be non empty SubSpace of X; ( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )
thus
( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )
( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )proof
assume A1:
X1,
X2 are_separated
;
( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) )
hence
X1 misses X2
by TSEP_1:63;
for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y
X1,
X2 are_weakly_separated
by A1, TSEP_1:78;
hence
for
Y being non
empty TopSpace for
f being
Function of
X,
Y st
f | X1 is
continuous Function of
X1,
Y &
f | X2 is
continuous Function of
X2,
Y holds
f | (X1 union X2) is
continuous Function of
(X1 union X2),
Y
by Th117;
verum
end;
thus
( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )
verumproof
assume A2:
X1 misses X2
;
( ex Y being non empty TopSpace ex f being Function of X,Y st
( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y & f | (X1 union X2) is not continuous Function of (X1 union X2),Y ) or X1,X2 are_separated )
assume A3:
for
Y being non
empty TopSpace for
f being
Function of
X,
Y st
f | X1 is
continuous Function of
X1,
Y &
f | X2 is
continuous Function of
X2,
Y holds
f | (X1 union X2) is
continuous Function of
(X1 union X2),
Y
;
X1,X2 are_separated
for
Y being non
empty TopSpace for
g being
Function of
(X1 union X2),
Y st
g | X1 is
continuous Function of
X1,
Y &
g | X2 is
continuous Function of
X2,
Y holds
g is
continuous Function of
(X1 union X2),
Y
proof
let Y be non
empty TopSpace;
for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds
g is continuous Function of (X1 union X2),Ylet g be
Function of
(X1 union X2),
Y;
( 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 )
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
consider h being
Function of
X,
Y such that A6:
h | (X1 union X2) = g
by Th57;
X2 is
SubSpace of
X1 union X2
by TSEP_1:22;
then A7:
h | X2 is
continuous Function of
X2,
Y
by A5, A6, Th70;
X1 is
SubSpace of
X1 union X2
by TSEP_1:22;
then
h | X1 is
continuous Function of
X1,
Y
by A4, A6, Th70;
hence
g is
continuous Function of
(X1 union X2),
Y
by A3, A6, A7;
verum
end;
hence
X1,
X2 are_separated
by A2, Th123;
verum
end;