let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X st X = X1 union X2 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 is continuous Function of X,Y ) ) )
let X1, X2 be non empty SubSpace of X; ( X = X1 union X2 implies ( 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 is continuous Function of X,Y ) ) ) )
assume A1:
X = X1 union X2
; ( 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 is continuous Function of X,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 is continuous Function of X,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 is continuous Function of X,Y ) implies X1,X2 are_separated )proof
assume A2:
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 is continuous Function of X,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 is continuous Function of X,Y
X1,
X2 are_weakly_separated
by A2, 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 is
continuous Function of
X,
Y
by A1, Th120;
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 is continuous Function of X,Y ) implies X1,X2 are_separated )
verumproof
assume A3:
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 is not continuous Function of X,Y ) or X1,X2 are_separated )
assume A4:
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 is
continuous Function of
X,
Y
;
X1,X2 are_separated
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
proof
let Y be 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),Ylet f be
Function of
X,
Y;
( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y implies f | (X1 union X2) is continuous Function of (X1 union X2),Y )
assume
(
f | X1 is
continuous Function of
X1,
Y &
f | X2 is
continuous Function of
X2,
Y )
;
f | (X1 union X2) is continuous Function of (X1 union X2),Y
then
f is
continuous Function of
X,
Y
by A4;
hence
f | (X1 union X2) is
continuous Function of
(X1 union X2),
Y
;
verum
end;
hence
X1,
X2 are_separated
by A3, Th124;
verum
end;