let X be non empty TopSpace; :: thesis: 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 f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )
thus
( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )
:: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )proof
assume A1:
X1,
X2 are_separated
;
:: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) )
then A2:
X1,
X2 are_weakly_separated
by TSEP_1:85;
thus
X1 misses X2
by A1, TSEP_1:68;
:: thesis: for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y
thus
for
Y being non
empty TopSpace for
f1 being
continuous Function of
X1,
Y for
f2 being
continuous Function of
X2,
Y holds
f1 union f2 is
continuous Function of
(X1 union X2),
Y
by A1, A2, Th145, TSEP_1:68;
:: thesis: verum
end;
thus
( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )
:: thesis: verumproof
assume A3:
X1 misses X2
;
:: thesis: ( ex Y being non empty TopSpace ex f1 being continuous Function of X1,Y ex f2 being continuous Function of X2,Y st f1 union f2 is not continuous Function of (X1 union X2),Y or X1,X2 are_separated )
assume A4:
for
Y being non
empty TopSpace for
f1 being
continuous Function of
X1,
Y for
f2 being
continuous Function of
X2,
Y holds
f1 union f2 is
continuous Function of
(X1 union X2),
Y
;
:: thesis: X1,X2 are_separated
now let Y be non
empty TopSpace;
:: thesis: 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;
:: 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 )assume A5:
(
g | X1 is
continuous Function of
X1,
Y &
g | X2 is
continuous Function of
X2,
Y )
;
:: thesis: g is continuous Function of (X1 union X2),Ythen reconsider f1 =
g | X1 as
continuous Function of
X1,
Y ;
reconsider f2 =
g | X2 as
continuous Function of
X2,
Y by A5;
g = f1 union f2
by Th138;
hence
g is
continuous Function of
(X1 union X2),
Y
by A4;
:: thesis: verum end;
hence
X1,
X2 are_separated
by A3, Th135;
:: thesis: verum
end;