:: Separated and Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received January 8, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

Lm1: for A being set
for B, C, D being Subset of A st B \ C = {} holds
B misses D \ C

proof end;

Lm2: for A, B, C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)

proof end;

theorem Th1: :: TSEP_1:1

for X being TopStruct
for X0 being SubSpace of X holds the carrier of X0 is Subset of X

proof end;

theorem Th2: :: TSEP_1:2

for X being TopStruct holds X is SubSpace of X

proof end;

theorem :: TSEP_1:3

for X being strict TopStruct holds X | ([#] X) = X

proof end;

theorem Th4: :: TSEP_1:4

for X being TopSpace
for X1, X2 being SubSpace of X holds
( the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2 )

proof end;

Lm3: for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X

proof end;

theorem Th5: :: TSEP_1:5

for X being TopStruct
for X1, X2 being SubSpace of X st the carrier of X1 = the carrier of X2 holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem :: TSEP_1:6

for X being TopSpace
for X1, X2 being SubSpace of X st X1 is SubSpace of X2 & X2 is SubSpace of X1 holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem Th7: :: TSEP_1:7

for X being TopSpace
for X1 being SubSpace of X
for X2 being SubSpace of X1 holds X2 is SubSpace of X

proof end;

theorem Th8: :: TSEP_1:8

for X being TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds
( B is closed iff A is closed )

proof end;

theorem Th9: :: TSEP_1:9

for X being TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( B is open iff A is open )

proof end;

theorem Th10: :: TSEP_1:10

for X being non empty TopStruct
for A0 being non empty Subset of X ex X0 being non empty strict SubSpace of X st A0 = the carrier of X0

proof end;

::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13).

theorem Th11: :: TSEP_1:11

for X being TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is closed SubSpace of X iff A is closed )

proof end;

theorem :: TSEP_1:12

for X being TopSpace
for X0 being closed SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is closed iff A is closed )

proof end;

theorem :: TSEP_1:13

for X being TopSpace
for X1 being closed SubSpace of X
for X2 being closed SubSpace of X1 holds X2 is closed SubSpace of X

proof end;

theorem :: TSEP_1:14

for X being non empty TopSpace
for X1 being non empty closed SubSpace of X
for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is non empty closed SubSpace of X2

proof end;

theorem Th15: :: TSEP_1:15

for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st A0 = the carrier of X0

proof end;

definition

let X be TopStruct ;
let IT be SubSpace of X;

attr IT is open means :Def1: :: TSEP_1:def 1
for A being Subset of X st A = the carrier of IT holds
A is open ;

end;

:: deftheorem Def1 defines open TSEP_1:def 1 :
for X being TopStruct
for IT being SubSpace of X holds
( IT is open iff for A being Subset of X st A = the carrier of IT holds
A is open );

Lm4: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T

proof end;

registration

let X be TopSpace;

cluster strict TopSpace-like open for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is strict & b₁ is open )

proof end;

end;

registration

let X be non empty TopSpace;

cluster non empty strict TopSpace-like open for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is strict & b₁ is open & not b₁ is empty )

proof end;

end;

::Properties of Open Subspaces.

theorem Th16: :: TSEP_1:16

for X being TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is open SubSpace of X iff A is open )

proof end;

theorem :: TSEP_1:17

for X being TopSpace
for X0 being open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is open iff A is open )

proof end;

theorem :: TSEP_1:18

for X being TopSpace
for X1 being open SubSpace of X
for X2 being open SubSpace of X1 holds X2 is open SubSpace of X

proof end;

theorem :: TSEP_1:19

for X being non empty TopSpace
for X1 being open SubSpace of X
for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is open SubSpace of X2

proof end;

theorem Th20: :: TSEP_1:20

for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is open holds
ex X0 being non empty strict open SubSpace of X st A0 = the carrier of X0

proof end;

definition

let X be non empty TopStruct ;
let X1, X2 be non empty SubSpace of X;

func X1 union X2 -> non empty strict SubSpace of X means :Def2: :: TSEP_1:def 2
the carrier of it = the carrier of X1 \/ the carrier of X2;

existence
ex b₁ being non empty strict SubSpace of X st the carrier of b₁ = the carrier of X1 \/ the carrier of X2

proof end;

uniqueness
for b₁, b₂ being non empty strict SubSpace of X st the carrier of b₁ = the carrier of X1 \/ the carrier of X2 & the carrier of b₂ = the carrier of X1 \/ the carrier of X2 holds
b₁ = b₂ by Th5;
commutativity
for b₁ being non empty strict SubSpace of X
for X1, X2 being non empty SubSpace of X st the carrier of b₁ = the carrier of X1 \/ the carrier of X2 holds
the carrier of b₁ = the carrier of X2 \/ the carrier of X1 ;

end;

:: deftheorem Def2 defines union TSEP_1:def 2 :
for X being non empty TopStruct
for X1, X2 being non empty SubSpace of X
for b₄ being non empty strict SubSpace of X holds
( b₄ = X1 union X2 iff the carrier of b₄ = the carrier of X1 \/ the carrier of X2 );

::Properties of the Union of two Subspaces.

theorem :: TSEP_1:21

for X being non empty TopSpace
for X1, X2, X3 being non empty SubSpace of X holds (X1 union X2) union X3 = X1 union (X2 union X3)

proof end;

theorem Th22: :: TSEP_1:22

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds X1 is SubSpace of X1 union X2

proof end;

theorem :: TSEP_1:23

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1 is SubSpace of X2 iff X1 union X2 = TopStruct(# the carrier of X2, the topology of X2 #) )

proof end;

theorem :: TSEP_1:24

for X being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X holds X1 union X2 is closed SubSpace of X

proof end;

theorem :: TSEP_1:25

for X being non empty TopSpace
for X1, X2 being non empty open SubSpace of X holds X1 union X2 is open SubSpace of X

proof end;

definition

let X1, X2 be 1-sorted ;

pred X1 misses X2 means :: TSEP_1:def 3
the carrier of X1 misses the carrier of X2;

correctness
;
symmetry
for X1, X2 being 1-sorted st the carrier of X1 misses the carrier of X2 holds
the carrier of X2 misses the carrier of X1 ;

end;

:: deftheorem defines misses TSEP_1:def 3 :
for X1, X2 being 1-sorted holds
( X1 misses X2 iff the carrier of X1 misses the carrier of X2 );

notation

let X1, X2 be 1-sorted ;
antonym X1 meets X2 for X1 misses X2;

end;

definition

let X be non empty TopStruct ;
let X1, X2 be non empty SubSpace of X;
assume A1: X1 meets X2 ;

func X1 meet X2 -> non empty strict SubSpace of X means :Def4: :: TSEP_1:def 4
the carrier of it = the carrier of X1 /\ the carrier of X2;

existence
ex b₁ being non empty strict SubSpace of X st the carrier of b₁ = the carrier of X1 /\ the carrier of X2

proof end;

uniqueness
for b₁, b₂ being non empty strict SubSpace of X st the carrier of b₁ = the carrier of X1 /\ the carrier of X2 & the carrier of b₂ = the carrier of X1 /\ the carrier of X2 holds
b₁ = b₂ by Th5;

end;

:: deftheorem Def4 defines meet TSEP_1:def 4 :
for X being non empty TopStruct
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
for b₄ being non empty strict SubSpace of X holds
( b₄ = X1 meet X2 iff the carrier of b₄ = the carrier of X1 /\ the carrier of X2 );

::Properties of the Meet of two Subspaces.

theorem Th26: :: TSEP_1:26

for X being non empty TopSpace
for X1, X2, X3 being non empty SubSpace of X holds
( ( X1 meets X2 implies X1 meet X2 = X2 meet X1 ) & ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) ) )

proof end;

theorem Th27: :: TSEP_1:27

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1 meet X2 is SubSpace of X1 & X1 meet X2 is SubSpace of X2 )

proof end;

theorem :: TSEP_1:28

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 is SubSpace of X2 implies X1 meet X2 = TopStruct(# the carrier of X1, the topology of X1 #) ) & ( X1 meet X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies X1 meet X2 = TopStruct(# the carrier of X2, the topology of X2 #) ) & ( X1 meet X2 = TopStruct(# the carrier of X2, the topology of X2 #) implies X2 is SubSpace of X1 ) )

proof end;

theorem :: TSEP_1:29

for X being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X st X1 meets X2 holds
X1 meet X2 is closed SubSpace of X

proof end;

theorem :: TSEP_1:30

for X being non empty TopSpace
for X1, X2 being non empty open SubSpace of X st X1 meets X2 holds
X1 meet X2 is open SubSpace of X

proof end;

::Connections between the Union and the Meet.

theorem :: TSEP_1:31

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is SubSpace of X1 union X2

proof end;

theorem :: TSEP_1:32

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets Y & Y meets X2 holds
( (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) & Y meet (X1 union X2) = (Y meet X1) union (Y meet X2) )

proof end;

theorem :: TSEP_1:33

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets X2 holds
( (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) & Y union (X1 meet X2) = (Y union X1) meet (Y union X2) )

proof end;

notation

let X be TopStruct ;
let A1, A2 be Subset of X;
antonym A1,A2 are_not_separated for A1,A2 are_separated ;

end;

::Properties of Separated Subsets of Topological Spaces.

theorem Th34: :: TSEP_1:34

for X being TopSpace
for A1, A2 being Subset of X st A1 is closed & A2 is closed holds
( A1 misses A2 iff A1,A2 are_separated )

proof end;

theorem Th35: :: TSEP_1:35

for X being TopSpace
for A1, A2 being Subset of X st A1 \/ A2 is closed & A1,A2 are_separated holds
( A1 is closed & A2 is closed )

proof end;

theorem Th36: :: TSEP_1:36

for X being TopSpace
for A1, A2 being Subset of X st A1 misses A2 & A1 is open holds
A1 misses Cl A2

proof end;

theorem Th37: :: TSEP_1:37

for X being TopSpace
for A1, A2 being Subset of X st A1 is open & A2 is open holds
( A1 misses A2 iff A1,A2 are_separated )

proof end;

theorem Th38: :: TSEP_1:38

for X being TopSpace
for A1, A2 being Subset of X st A1 \/ A2 is open & A1,A2 are_separated holds
( A1 is open & A2 is open )

proof end;

theorem Th39: :: TSEP_1:39

for X being TopSpace
for A1, A2, C being Subset of X st A1,A2 are_separated holds
A1 /\ C,A2 /\ C are_separated

proof end;

theorem Th40: :: TSEP_1:40

for X being TopSpace
for A1, A2, B being Subset of X st ( A1,B are_separated or A2,B are_separated ) holds
A1 /\ A2,B are_separated

proof end;

theorem Th41: :: TSEP_1:41

for X being TopSpace
for A1, A2, B being Subset of X holds
( ( A1,B are_separated & A2,B are_separated ) iff A1 \/ A2,B are_separated )

proof end;

theorem Th42: :: TSEP_1:42

for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) )

proof end;

::First Characterization of Separated Subsets of Topological Spaces.

theorem Th43: :: TSEP_1:43

for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed ) )

proof end;

theorem Th44: :: TSEP_1:44

for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open ) )

proof end;

::Second Characterization of Separated Subsets of Topological Spaces.

theorem Th45: :: TSEP_1:45

for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open ) )

proof end;

definition

let X be TopStruct ;
let A1, A2 be Subset of X;

pred A1,A2 are_weakly_separated means :: TSEP_1:def 5
A1 \ A2,A2 \ A1 are_separated ;

symmetry
for A1, A2 being Subset of X st A1 \ A2,A2 \ A1 are_separated holds
A2 \ A1,A1 \ A2 are_separated ;

end;

:: deftheorem defines are_weakly_separated TSEP_1:def 5 :
for X being TopStruct
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 \ A2,A2 \ A1 are_separated );

notation

let X be TopStruct ;
let A1, A2 be Subset of X;
antonym A1,A2 are_not_weakly_separated for A1,A2 are_weakly_separated ;

end;

::Properties of Weakly Separated Subsets of Topological Spaces.

theorem Th46: :: TSEP_1:46

for X being TopSpace
for A1, A2 being Subset of X holds
( ( A1 misses A2 & A1,A2 are_weakly_separated ) iff A1,A2 are_separated )

proof end;

theorem Th47: :: TSEP_1:47

for X being TopSpace
for A1, A2 being Subset of X st A1 c= A2 holds
A1,A2 are_weakly_separated

proof end;

theorem Th48: :: TSEP_1:48

for X being TopSpace
for A1, A2 being Subset of X st A1 is closed & A2 is closed holds
A1,A2 are_weakly_separated

proof end;

theorem Th49: :: TSEP_1:49

for X being TopSpace
for A1, A2 being Subset of X st A1 is open & A2 is open holds
A1,A2 are_weakly_separated

proof end;

::Extension Theorems for Weakly Separated Subsets.

theorem Th50: :: TSEP_1:50

for X being TopSpace
for A1, A2, C being Subset of X st A1,A2 are_weakly_separated holds
A1 \/ C,A2 \/ C are_weakly_separated

proof end;

theorem Th51: :: TSEP_1:51

for X being TopSpace
for A1, A2, B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 & A1,A2 are_weakly_separated holds
A1 \/ B1,A2 \/ B2 are_weakly_separated

proof end;

theorem Th52: :: TSEP_1:52

for X being TopSpace
for A1, A2, B being Subset of X st A1,B are_weakly_separated & A2,B are_weakly_separated holds
A1 /\ A2,B are_weakly_separated

proof end;

theorem Th53: :: TSEP_1:53

for X being TopSpace
for A1, A2, B being Subset of X st A1,B are_weakly_separated & A2,B are_weakly_separated holds
A1 \/ A2,B are_weakly_separated

proof end;

::First Characterization of Weakly Separated Subsets of Topological Spaces.

theorem Th54: :: TSEP_1:54

for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open ) )

proof end;

theorem Th55: :: TSEP_1:55

for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) )

proof end;

theorem Th56: :: TSEP_1:56

for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) )

proof end;

theorem Th57: :: TSEP_1:57

for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open ) ) )

proof end;

::Second Characterization of Weakly Separated Subsets of Topological Spaces.

theorem Th58: :: TSEP_1:58

for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )

proof end;

theorem Th59: :: TSEP_1:59

for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) )

proof end;

theorem Th60: :: TSEP_1:60

for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is open & C2 is open & C is closed ) )

proof end;

theorem Th61: :: TSEP_1:61

for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is open & C2 is open & C1 c= A1 & C2 c= A2 & ( A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) ) )

proof end;

::A Characterization of Separated Subsets by means of Weakly Separated ones.

theorem Th62: :: TSEP_1:62

for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) )

proof end;

definition

let X be TopStruct ;
let X1, X2 be SubSpace of X;

pred X1,X2 are_separated means :: TSEP_1:def 6
for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated ;

symmetry
for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated ) holds
for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds
A1,A2 are_separated ;

end;

:: deftheorem defines are_separated TSEP_1:def 6 :
for X being TopStruct
for X1, X2 being SubSpace of X holds
( X1,X2 are_separated iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated );

notation

let X be TopStruct ;
let X1, X2 be SubSpace of X;
antonym X1,X2 are_not_separated for X1,X2 are_separated ;

end;

::Properties of Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:63

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 are_separated holds
X1 misses X2

proof end;

theorem :: TSEP_1:64

for X being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X holds
( X1 misses X2 iff X1,X2 are_separated )

proof end;

theorem :: TSEP_1:65

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_separated holds
X1 is closed SubSpace of X

proof end;

theorem :: TSEP_1:66

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 union X2 is closed SubSpace of X & X1,X2 are_separated holds
X1 is closed SubSpace of X

proof end;

theorem :: TSEP_1:67

for X being non empty TopSpace
for X1, X2 being non empty open SubSpace of X holds
( X1 misses X2 iff X1,X2 are_separated )

proof end;

theorem :: TSEP_1:68

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_separated holds
X1 is open SubSpace of X

proof end;

theorem :: TSEP_1:69

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 union X2 is open SubSpace of X & X1,X2 are_separated holds
X1 is open SubSpace of X

proof end;

::Restriction Theorems for Separated Subspaces.

theorem :: TSEP_1:70

for X being non empty TopSpace
for Y, X1, X2 being non empty SubSpace of X st X1 meets Y & X2 meets Y & X1,X2 are_separated holds
( X1 meet Y,X2 meet Y are_separated & Y meet X1,Y meet X2 are_separated )

proof end;

theorem Th71: :: TSEP_1:71

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for Y1, Y2 being SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & X1,X2 are_separated holds
Y1,Y2 are_separated

proof end;

theorem :: TSEP_1:72

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets X2 & X1,Y are_separated holds
X1 meet X2,Y are_separated

proof end;

theorem :: TSEP_1:73

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X holds
( ( X1,Y are_separated & X2,Y are_separated ) iff X1 union X2,Y are_separated )

proof end;

theorem :: TSEP_1:74

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty closed SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )

proof end;

::First Characterization of Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:75

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty closed SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )

proof end;

theorem :: TSEP_1:76

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )

proof end;

::Second Characterization of Separated Subspaces of Topological Spaces.

theorem Th77: :: TSEP_1:77

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )

proof end;

definition

let X be TopStruct ;
let X1, X2 be SubSpace of X;

pred X1,X2 are_weakly_separated means :: TSEP_1:def 7
for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated ;

symmetry
for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated ) holds
for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds
A1,A2 are_weakly_separated ;

end;

:: deftheorem defines are_weakly_separated TSEP_1:def 7 :
for X being TopStruct
for X1, X2 being SubSpace of X holds
( X1,X2 are_weakly_separated iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated );

notation

let X be TopStruct ;
let X1, X2 be SubSpace of X;
antonym X1,X2 are_not_weakly_separated for X1,X2 are_weakly_separated ;

end;

::Properties of Weakly Separated Subspaces of Topological Spaces.

theorem Th78: :: TSEP_1:78

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( ( X1 misses X2 & X1,X2 are_weakly_separated ) iff X1,X2 are_separated )

proof end;

theorem Th79: :: TSEP_1:79

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1,X2 are_weakly_separated by Th47, Th4;

theorem Th80: :: TSEP_1:80

for X being non empty TopSpace
for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated

proof end;

theorem Th81: :: TSEP_1:81

for X being non empty TopSpace
for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated

proof end;

::Extension Theorems for Weakly Separated Subspaces.

theorem :: TSEP_1:82

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1,X2 are_weakly_separated holds
X1 union Y,X2 union Y are_weakly_separated

proof end;

theorem :: TSEP_1:83

for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X2 & Y2 is SubSpace of X1 & X1,X2 are_weakly_separated holds
( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated )

proof end;

theorem :: TSEP_1:84

for X being non empty TopSpace
for Y, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated ) )

proof end;

theorem :: TSEP_1:85

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X holds
( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 union X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 union X2 are_weakly_separated ) )

proof end;

::First Characterization of Weakly Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:86

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty open SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )

proof end;

theorem :: TSEP_1:87

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )

proof end;

theorem :: TSEP_1:88

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 misses X2 holds
( X1,X2 are_weakly_separated iff ( X1 is closed SubSpace of X & X2 is closed SubSpace of X ) )

proof end;

::Second Characterization of Weakly Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:89

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )

proof end;

theorem :: TSEP_1:90

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )

proof end;

theorem :: TSEP_1:91

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 misses X2 holds
( X1,X2 are_weakly_separated iff ( X1 is open SubSpace of X & X2 is open SubSpace of X ) )

proof end;

::A Characterization of Separated Subspaces by means of Weakly Separated ones.

theorem :: TSEP_1:92

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty SubSpace of X st
( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )

proof end;

theorem :: TSEP_1:93

for T being TopStruct holds T | ([#] T) = TopStruct(# the carrier of T, the topology of T #)

proof end;