The abstract of the Mizar article:

Left and Right Component of the Complement of a Special Closed Curve

by

Andrzej Trybulec

Received October 29, 1995

MML identifier: GOBOARD9

[ Mizar article, MML identifier index ]

environ

 vocabulary SEQM_3, GOBOARD5, PRE_TOPC, EUCLID, GOBOARD1, ARYTM_1, CONNSP_1,
      BOOLE, RELAT_1, SUBSET_1, RELAT_2, TOPREAL1, JORDAN1, FINSEQ_1, FINSEQ_5,
      FUNCT_1, MCART_1, GOBOARD2, CARD_1, MATRIX_1, ABSVALUE, FINSEQ_6, ARYTM,
      TREES_1, TOPS_1, ARYTM_3, GOBOARD9, FINSEQ_4, ORDINAL2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, ABSVALUE, BINARITH, FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1,
      CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, EUCLID, TOPREAL1, GOBOARD1,
      GOBOARD2, JORDAN1, FINSEQ_5, FINSEQ_6, GOBOARD5;
 constructors SEQM_3, REAL_1, ABSVALUE, BINARITH, TOPS_1, CONNSP_1, GOBOARD2,
      JORDAN1, FINSEQ_5, GOBOARD5, FINSEQ_4, INT_1, MEMBERED;
 clusters STRUCT_0, GOBOARD5, RELSET_1, PRE_TOPC, GOBOARD2, FINSEQ_6, EUCLID,
      FINSEQ_1, TOPREAL1, INT_1, XREAL_0, MEMBERED, ARYTM_3;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve f for non constant standard special_circular_sequence,
        i,j,k,i1,i2,j1,j2 for Nat,
        r,s,r1,s1,r2,s2 for Real,
        a,b for natural number,
        p,q for Point of TOP-REAL 2,
        G for Go-board;

theorem :: GOBOARD9:1
 a -' a = 0;

theorem :: GOBOARD9:2
 a -' b <= a;

theorem :: GOBOARD9:3
 for GX being non empty TopSpace, A1,A2,B being Subset of GX
  st A1 is_a_component_of B & A2 is_a_component_of B
 holds A1 = A2 or A1 misses A2;

theorem :: GOBOARD9:4
 for GX being non empty TopSpace,
     A,B being non empty Subset of GX,
     AA being Subset of GX|B st A = AA holds GX|A = GX|B|AA;

theorem :: GOBOARD9:5
 for GX being non empty TopSpace,
     A being non empty Subset of GX,
     B being non empty Subset of GX
  st A c= B & A is connected
 ex C being Subset of GX st C is_a_component_of B & A c= C;

theorem :: GOBOARD9:6
 for GX being non empty TopSpace, A,C,D being Subset of GX,
  B being Subset of GX st B is connected & C is_a_component_of D
      & A c= C & A meets B & B c= D
  holds B c= C;

theorem :: GOBOARD9:7
 LSeg(p,q) is convex;

theorem :: GOBOARD9:8
 LSeg(p,q) is connected;

definition
 cluster convex non empty Subset of TOP-REAL 2;
end;

theorem :: GOBOARD9:9
 for P,Q being convex Subset of TOP-REAL 2 holds P /\ Q is convex;

theorem :: GOBOARD9:10
for f being FinSequence of TOP-REAL 2
 holds Rev X_axis f = X_axis Rev f;

theorem :: GOBOARD9:11
for f being FinSequence of TOP-REAL 2
 holds Rev Y_axis f = Y_axis Rev f;

definition
 cluster non constant FinSequence;
end;

definition let f be non constant FinSequence;
 cluster Rev f -> non constant;
end;

definition let f be standard special_circular_sequence;
 redefine func Rev f -> standard special_circular_sequence;
end;

theorem :: GOBOARD9:12
 i >= 1 & j >= 1 & i+j = len f implies left_cell(f,i) = right_cell(Rev f,j);

theorem :: GOBOARD9:13
 i >= 1 & j >= 1 & i+j = len f implies left_cell(Rev f,i) = right_cell(f,j);

theorem :: GOBOARD9:14
 1 <= k & k+1 <= len f implies
  ex i,j st i <= len GoB f & j <=
 width GoB f & cell(GoB f,i,j) = left_cell(f,k);

theorem :: GOBOARD9:15
  j <= width G implies Int h_strip(G,j) is convex;

theorem :: GOBOARD9:16
  i <= len G implies Int v_strip(G,i) is convex;

theorem :: GOBOARD9:17
 i <= len G & j <= width G implies Int cell(G,i,j) <> {};

theorem :: GOBOARD9:18
 1 <= k & k+1 <= len f implies Int left_cell(f,k) <> {};

theorem :: GOBOARD9:19
 1 <= k & k+1 <= len f implies Int right_cell(f,k) <> {};

theorem :: GOBOARD9:20
 i <= len G & j <= width G implies Int cell(G,i,j) is convex;

theorem :: GOBOARD9:21
 i <= len G & j <= width G implies Int cell(G,i,j) is connected;

theorem :: GOBOARD9:22
 1 <= k & k+1 <= len f implies Int left_cell(f,k) is connected;

theorem :: GOBOARD9:23
 1 <= k & k+1 <= len f implies Int right_cell(f,k) is connected;

definition let f;
 func LeftComp f -> Subset of TOP-REAL 2 means
:: GOBOARD9:def 1
 it is_a_component_of (L~f)` & Int left_cell(f,1) c= it;
 func RightComp f -> Subset of TOP-REAL 2 means
:: GOBOARD9:def 2
  it is_a_component_of (L~f)` & Int right_cell(f,1) c= it;
end;

theorem :: GOBOARD9:24
 for k st 1 <= k & k+1 <= len f holds Int left_cell(f,k) c= LeftComp f;

theorem :: GOBOARD9:25
   GoB Rev f = GoB f;

theorem :: GOBOARD9:26
 RightComp f = LeftComp Rev f;

theorem :: GOBOARD9:27
   RightComp Rev f = LeftComp f;

theorem :: GOBOARD9:28
   for k st 1 <= k & k+1 <= len f holds Int right_cell(f,k) c= RightComp f;