The abstract of the Mizar article:

On a Duality Between Weakly Separated Subspaces of Topological Spaces

by

Zbigniew Karno

Received November 9, 1992

MML identifier: TSEP_2

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, BOOLE, SUBSET_1, TOPS_1, TSEP_1, CONNSP_1, TARSKI,
      SETFAM_1, TSEP_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, STRUCT_0, TOPS_1, BORSUK_1,
      TSEP_1;
 constructors CONNSP_1, TOPS_1, BORSUK_1, TSEP_1, MEMBERED;
 clusters PRE_TOPC, STRUCT_0, MEMBERED, ZFMISC_1;
 requirements BOOLE, SUBSET;


begin
:: 1. Certain Set-Decompositions of a Topological Space.
reserve X for non empty TopSpace;

theorem :: TSEP_2:1
 for A, B being Subset of X holds ( A`) \  B` = B \ A;

::Complemented Subsets.
definition let X be TopSpace, A1, A2 be Subset of X;
   pred A1,A2 constitute_a_decomposition means
:: TSEP_2:def 1
 A1 misses A2 & A1 \/ A2 = the carrier of X;
 symmetry;
 antonym A1,A2 do_not_constitute_a_decomposition;
end;

reserve A, A1, A2, B1, B2 for Subset of X;

theorem :: TSEP_2:2
 A1,A2 constitute_a_decomposition iff A1 misses A2 & A1 \/ A2 = [#]X;

canceled;

theorem :: TSEP_2:4
 A1,A2 constitute_a_decomposition implies A1 =  A2` & A2 =  A1`;

theorem :: TSEP_2:5
 A1 =  A2` or A2 =  A1` implies A1,A2 constitute_a_decomposition;

theorem :: TSEP_2:6
 A, A` constitute_a_decomposition;

theorem :: TSEP_2:7
   {}X,[#]X constitute_a_decomposition;

theorem :: TSEP_2:8
 A,A do_not_constitute_a_decomposition;

definition let X be non empty TopSpace, A1, A2 be Subset of X;
 redefine pred A1,A2 constitute_a_decomposition;
 irreflexivity;
end;

theorem :: TSEP_2:9
 A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition
  implies A1 = A2;

theorem :: TSEP_2:10
 A1,A2 constitute_a_decomposition implies
   (Cl A1),(Int A2) constitute_a_decomposition &
    (Int A1),(Cl A2) constitute_a_decomposition;

theorem :: TSEP_2:11
   (Cl A),(Int  A`) constitute_a_decomposition &
  (Cl  A`),(Int A) constitute_a_decomposition &
     (Int A),(Cl  A`) constitute_a_decomposition &
      (Int  A`),(Cl A) constitute_a_decomposition;

theorem :: TSEP_2:12
 for A1, A2 being Subset of X st
  A1,A2 constitute_a_decomposition holds (A1 is open iff A2 is closed);

theorem :: TSEP_2:13
   for A1, A2 being Subset of X st
  A1,A2 constitute_a_decomposition holds (A1 is closed iff A2 is open);

theorem :: TSEP_2:14
 A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies
  (A1 /\ B1),(A2 \/ B2) constitute_a_decomposition;

theorem :: TSEP_2:15
   A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies
  (A1 \/ B1),(A2 /\ B2) constitute_a_decomposition;

begin
:: 2. A Duality Between Pairs of Weakly Separated Subsets.
reserve X for non empty TopSpace, A1, A2 for Subset of X;

theorem :: TSEP_2:16
 for A1, A2, C1, C2 being Subset of X st
  A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds
   A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated;

theorem :: TSEP_2:17
   A1,A2 are_weakly_separated iff  A1`, A2` are_weakly_separated;

theorem :: TSEP_2:18
   for A1, A2, C1, C2 being Subset of X st
  A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds
   A1,A2 are_separated implies C1,C2 are_weakly_separated;

theorem :: TSEP_2:19
 for A1, A2, C1, C2 being Subset of X st
  A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds
    A1 misses A2 & C1,C2 are_weakly_separated implies A1,A2 are_separated;

theorem :: TSEP_2:20
   for A1, A2, C1, C2 being Subset of X st
  A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds
    C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated implies
      A1,A2 are_separated;

theorem :: TSEP_2:21
   A1,A2 constitute_a_decomposition implies
  (A1,A2 are_weakly_separated iff A1,A2 are_separated);

theorem :: TSEP_2:22
 A1,A2 are_weakly_separated iff
   (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated;

::An Enlargement Theorem for Subsets.
theorem :: TSEP_2:23
 for A1, A2, C1, C2 being Subset of X st
  C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 holds
   C1,C2 are_weakly_separated implies A1,A2 are_weakly_separated;

theorem :: TSEP_2:24
 A1,A2 are_weakly_separated iff
   A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated;

::An Extenuation Theorem for Subsets.
theorem :: TSEP_2:25
 for A1, A2, C1, C2 being Subset of X st
  C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 holds
   A1,A2 are_weakly_separated implies C1,C2 are_weakly_separated;

::Separated and Weakly Separated Subsets in Subspaces.
reserve X0 for non empty SubSpace of X, B1, B2 for Subset of X0;

theorem :: TSEP_2:26
 B1 = A1 & B2 = A2 implies
   (A1,A2 are_separated iff B1,B2 are_separated);

theorem :: TSEP_2:27
 B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2 implies
   (A1,A2 are_separated implies B1,B2 are_separated);

theorem :: TSEP_2:28
 B1 = A1 & B2 = A2 implies
   (A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated);

theorem :: TSEP_2:29
 B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2 implies
   (A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated);


begin
:: 3. Certain Subspace-Decompositions of a Topological Space.

definition let X be non empty TopSpace, X1, X2 be SubSpace of X;
   pred X1,X2 constitute_a_decomposition means
:: TSEP_2:def 2
 for A1, A2 being Subset of X st
   A1 = the carrier of X1 & A2 = the carrier of X2 holds
    A1,A2 constitute_a_decomposition;
 symmetry;
 antonym X1,X2 do_not_constitute_a_decomposition;
end;
reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X;

theorem :: TSEP_2:30
 X1,X2 constitute_a_decomposition iff
  X1 misses X2 & the TopStruct of X = X1 union X2;

canceled;

theorem :: TSEP_2:32
 X0,X0 do_not_constitute_a_decomposition;

definition let X be non empty TopSpace, A1, A2 be non empty SubSpace of X;
 redefine pred A1,A2 constitute_a_decomposition;
 irreflexivity;
end;

theorem :: TSEP_2:33
   X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition
  implies the TopStruct of X1 = the TopStruct of X2;

theorem :: TSEP_2:34
 for X1, X2, Y1, Y2 being non empty SubSpace of X st
  X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
    Y1 union Y2 = the TopStruct of X iff X1 misses X2;

theorem :: TSEP_2:35
 X1,X2 constitute_a_decomposition implies (X1 is open iff X2 is closed);

theorem :: TSEP_2:36
   X1,X2 constitute_a_decomposition implies (X1 is closed iff X2 is open);

theorem :: TSEP_2:37
 X1 meets Y1 &
  X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition implies
   (X1 meet Y1),(X2 union Y2) constitute_a_decomposition;

theorem :: TSEP_2:38
   X2 meets Y2 &
  X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition implies
   (X1 union Y1),(X2 meet Y2) constitute_a_decomposition;

begin
:: 4. A Duality Between Pairs of Weakly Separated Subspaces.
reserve X for non empty TopSpace;

theorem :: TSEP_2:39
 for X1, X2, Y1, Y2 being SubSpace of X st
  X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
   X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated;

theorem :: TSEP_2:40
   for X1, X2, Y1, Y2 being non empty SubSpace of X st
  X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
   X1,X2 are_separated implies Y1,Y2 are_weakly_separated;

theorem :: TSEP_2:41
 for X1, X2, Y1, Y2 being non empty SubSpace of X st
  X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
    X1 misses X2 & Y1,Y2 are_weakly_separated implies X1,X2 are_separated;

theorem :: TSEP_2:42
   for X1, X2, Y1, Y2 being non empty SubSpace of X st
  X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
    Y1 union Y2 = the TopStruct of X & Y1,Y2 are_weakly_separated implies
      X1,X2 are_separated;

theorem :: TSEP_2:43
   for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition
 holds (X1,X2 are_weakly_separated iff X1,X2 are_separated);

::An Enlargement Theorem for Subspaces.
theorem :: TSEP_2:44
   for X1, X2, Y1, Y2 being non empty SubSpace of X st
  Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 holds
    Y1,Y2 are_weakly_separated implies X1,X2 are_weakly_separated;

::An Extenuation Theorem for Subspaces.
theorem :: TSEP_2:45
   for X1, X2, Y1, Y2 being non empty SubSpace of X st
    Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
     Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 holds
   X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated;

::Separated and Weakly Separated Subspaces in Subspaces.
reserve X0 for non empty SubSpace of X;

theorem :: TSEP_2:46
 for X1, X2 being SubSpace of X, Y1, Y2 being SubSpace of X0 st
  the carrier of X1 = the carrier of Y1 &
   the carrier of X2 = the carrier of Y2 holds
  X1,X2 are_separated iff Y1,Y2 are_separated;

theorem :: TSEP_2:47
   for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0
  for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 holds
   X1,X2 are_separated implies Y1,Y2 are_separated;

theorem :: TSEP_2:48
   for X1, X2 being SubSpace of X, Y1, Y2 being SubSpace of X0 st
  the carrier of X1 = the carrier of Y1 &
   the carrier of X2 = the carrier of Y2 holds
   X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated;

theorem :: TSEP_2:49
   for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0
  for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 holds
   X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated;