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 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 ) ) )
let X1, X2 be non empty SubSpace of X; ( X1,X2 are_separated iff ( X1 misses X2 & ( 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 ) ) )
thus
( X1,X2 are_separated implies ( X1 misses X2 & ( 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 ) ) )
( X1 misses X2 & ( 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 ) implies X1,X2 are_separated )proof
assume A1:
X1,
X2 are_separated
;
( X1 misses X2 & ( 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 ) )
hence
X1 misses X2
by TSEP_1:63;
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
X1,
X2 are_weakly_separated
by A1, TSEP_1:78;
hence
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
by Th114;
verum
end;
thus
( X1 misses X2 & ( 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 ) implies X1,X2 are_separated )
verumproof
reconsider Y1 =
X1,
Y2 =
X2 as
SubSpace of
X1 union X2 by TSEP_1:22;
reconsider A2 = the
carrier of
X2 as
Subset of
X by TSEP_1:1;
reconsider A1 = the
carrier of
X1 as
Subset of
X by TSEP_1:1;
A2:
the
carrier of
(X1 union X2) = A1 \/ A2
by TSEP_1:def 2;
then reconsider C1 =
A1 as
Subset of
(X1 union X2) by XBOOLE_1:7;
reconsider C2 =
A2 as
Subset of
(X1 union X2) by A2, XBOOLE_1:7;
A3:
Cl C1 = (Cl A1) /\ ([#] (X1 union X2))
by PRE_TOPC:17;
A4:
Cl C2 = (Cl A2) /\ ([#] (X1 union X2))
by PRE_TOPC:17;
assume
X1 misses X2
;
( ex Y being non empty TopSpace ex 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 & g is not continuous Function of (X1 union X2),Y ) or X1,X2 are_separated )
then A5:
C1 misses C2
by TSEP_1:def 3;
assume A6:
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
;
X1,X2 are_separated
assume
X1,
X2 are_not_separated
;
contradiction
then A7:
ex
A10,
A20 being
Subset of
X st
(
A10 = the
carrier of
X1 &
A20 = the
carrier of
X2 &
A10,
A20 are_not_separated )
by TSEP_1:def 6;
A8:
now not C1,C2 are_separated assume A9:
C1,
C2 are_separated
;
contradictionthen
(Cl A1) /\ ([#] (X1 union X2)) misses A2
by A3, CONNSP_1:def 1;
then
((Cl A1) /\ ([#] (X1 union X2))) /\ A2 = {}
;
then A10:
((Cl A1) /\ A2) /\ ([#] (X1 union X2)) = {}
by XBOOLE_1:16;
A1 misses (Cl A2) /\ ([#] (X1 union X2))
by A4, A9, CONNSP_1:def 1;
then
A1 /\ ((Cl A2) /\ ([#] (X1 union X2))) = {}
;
then A11:
(A1 /\ (Cl A2)) /\ ([#] (X1 union X2)) = {}
by XBOOLE_1:16;
(
C1 c= [#] (X1 union X2) &
A1 /\ (Cl A2) c= A1 )
by XBOOLE_1:17;
then
A1 /\ (Cl A2) = {}
by A11, XBOOLE_1:1, XBOOLE_1:28;
then A12:
A1 misses Cl A2
;
(
C2 c= [#] (X1 union X2) &
(Cl A1) /\ A2 c= A2 )
by XBOOLE_1:17;
then
(Cl A1) /\ A2 = {}
by A10, XBOOLE_1:1, XBOOLE_1:28;
then
Cl A1 misses A2
;
hence
contradiction
by A7, A12, CONNSP_1:def 1;
verum end;
now contradictionper cases
( not C1 is open or not C2 is open )
by A8, A5, TSEP_1:37;
suppose A13:
not
C1 is
open
;
contradictionset g =
modid (
(X1 union X2),
C1);
set Y =
(X1 union X2) modified_with_respect_to C1;
(modid ((X1 union X2),C1)) | Y1 = (modid ((X1 union X2),C1)) | X1
by Def5;
then A14:
(modid ((X1 union X2),C1)) | X1 is
continuous Function of
X1,
((X1 union X2) modified_with_respect_to C1)
by Th100;
(modid ((X1 union X2),C1)) | Y2 = (modid ((X1 union X2),C1)) | X2
by Def5;
then A15:
(modid ((X1 union X2),C1)) | X2 is
continuous Function of
X2,
((X1 union X2) modified_with_respect_to C1)
by A5, Th99;
modid (
(X1 union X2),
C1) is not
continuous Function of
(X1 union X2),
((X1 union X2) modified_with_respect_to C1)
by A13, Th101;
hence
contradiction
by A6, A14, A15;
verum end; suppose A16:
not
C2 is
open
;
contradictionset g =
modid (
(X1 union X2),
C2);
set Y =
(X1 union X2) modified_with_respect_to C2;
(modid ((X1 union X2),C2)) | Y2 = (modid ((X1 union X2),C2)) | X2
by Def5;
then A17:
(modid ((X1 union X2),C2)) | X2 is
continuous Function of
X2,
((X1 union X2) modified_with_respect_to C2)
by Th100;
(modid ((X1 union X2),C2)) | Y1 = (modid ((X1 union X2),C2)) | X1
by Def5;
then A18:
(modid ((X1 union X2),C2)) | X1 is
continuous Function of
X1,
((X1 union X2) modified_with_respect_to C2)
by A5, Th99;
modid (
(X1 union X2),
C2) is not
continuous Function of
(X1 union X2),
((X1 union X2) modified_with_respect_to C2)
by A16, Th101;
hence
contradiction
by A6, A18, A17;
verum end;
hence
contradiction
;
verum
end;