The abstract of the Mizar article:

The First Part of Jordan's Theorem for Special Polygons

by

Yatsuka Nakamura, and

Andrzej Trybulec

Received July 22, 1996

MML identifier: GOBRD12

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, SEQM_3, GOBOARD5, ARYTM_3, EUCLID, MCART_1, RELAT_1,
      SUBSET_1, TOPREAL1, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, BOOLE, CONNSP_3,
      RELAT_2, GOBOARD9, CONNSP_1, TARSKI, MATRIX_1, ARYTM_1, GOBRD10, FUNCT_1,
      FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, GOBOARD1, NUMBERS,
      XREAL_0, STRUCT_0, REAL_1, NAT_1, BINARITH, PRE_TOPC, FUNCT_1, FINSEQ_1,
      FINSEQ_4, MATRIX_1, TOPS_1, CONNSP_1, EUCLID, GOBOARD2, GOBOARD5,
      GOBOARD9, CONNSP_3, GOBRD10;
 constructors REAL_1, BINARITH, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3,
      GOBRD10, FINSEQ_4, MEMBERED;
 clusters SUBSET_1, GOBOARD5, RELSET_1, PRE_TOPC, GOBOARD2, EUCLID, XREAL_0,
      GOBRD11, NAT_1, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

reserve i,j,k,k1,k2,i1,i2,j1,j2 for Nat,
        r,s for Real,
        x for set,

        f for non constant standard special_circular_sequence;

canceled;

theorem :: GOBRD12:2
for i,j st i<=len GoB f & j<=width GoB f
 holds Int cell(GoB f,i,j)c=(L~f)`;

theorem :: GOBRD12:3
 for i,j st i<=len GoB f & j<=width GoB f holds
   Cl Down(Int cell(GoB f,i,j),(L~f)`)=cell(GoB f,i,j)/\((L~f)`);

theorem :: GOBRD12:4
 for i,j st i<=len GoB f & j<=width GoB f holds
   Cl Down(Int cell(GoB f,i,j),(L~f)`) is connected
   & Down(Int cell(GoB f,i,j),(L~f)`)=Int cell(GoB f,i,j);

theorem :: GOBRD12:5
  (L~f)`=union {Cl Down(Int cell(GoB f,i,j),(L~f)`):
                          i<=len GoB f & j<=width GoB f};

theorem :: GOBRD12:6
Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`)
            is a_union_of_components of (TOP-REAL 2)|((L~f)`)
 & Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(L~f)`)=RightComp f;

theorem :: GOBRD12:7
 for i1,j1,i2,j2 st i1<=len GoB f & j1<=width GoB f
  & i2<=len GoB f & j2<=width GoB f & i1,j1,i2,j2 are_adjacent2
  holds Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f
    iff Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f;

theorem :: GOBRD12:8
 for F1,F2 being FinSequence of NAT st len F1=len F2 &
   (ex i st i in dom F1 & Int cell(GoB f,F1/.i,F2/.i)
                                c=LeftComp f \/ RightComp f)&
   (for i st 1<=i & i<len F1 holds
       F1/.i,F2/.i,F1/.(i+1),F2/.(i+1) are_adjacent2)&
   (for i,k1,k2 st i in dom F1 & k1=F1.i & k2=F2.i holds
        k1<=len GoB f & k2<=width GoB f)
   holds (for i st i in dom F1 holds
   Int cell(GoB f,F1/.i,F2/.i)c=LeftComp f \/ RightComp f);

theorem :: GOBRD12:9
  ex i,j st i<=len GoB f & j<=width GoB f &
  Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f;

theorem :: GOBRD12:10
  for i,j st i<=len GoB f & j<=width GoB f holds
  Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f;

theorem :: GOBRD12:11
   (L~f)`=LeftComp f \/ RightComp f;