:: The First Part of Jordan's Theorem for Special Polygons :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received July 22, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, FUNCT_1, GOBOARD5, TOPREAL1, STRUCT_0, EUCLID, RELAT_1, XXREAL_0, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, TARSKI, XBOOLE_0, PRE_TOPC, CONNSP_3, RELAT_2, GOBOARD9, CONNSP_1, ARYTM_3, CARD_1, RLTOPSP1, PARTFUN1, MATRIX_1, ZFMISC_1, MCART_1, ARYTM_1, RCOMP_1, NAT_1, CONVEX1, CHORD; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, ORDINAL1, NUMBERS, DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1, NAT_1, NAT_D, PRE_TOPC, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, TOPS_1, CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD2, GOBOARD5, GOBOARD9, CONNSP_3, GOBRD10, XXREAL_0; constructors DOMAIN_1, REAL_1, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3, GOBRD10, GOBOARD1, NAT_D, RELSET_1, CONVEX1; registrations SUBSET_1, RELSET_1, XXREAL_0, NAT_1, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, GOBOARD5, GOBRD11, JORDAN1, XREAL_0, ORDINAL1; requirements NUMERALS, REAL, SUBSET, 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; theorem :: GOBRD12:1 for i,j st i<=len GoB f & j<=width GoB f holds Int cell(GoB f,i,j )c=(L~f)`; theorem :: GOBRD12:2 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:3 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:4 (L~f)`=union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j<=width GoB f}; theorem :: GOBRD12:5 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:6 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_adjacent 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:7 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,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:8 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:9 for i,j st i<=len GoB f & j<=width GoB f holds Int cell(GoB f,i, j) c= LeftComp f \/ RightComp f; ::$N Jordan Curve Theorem for special polygons theorem :: GOBRD12:10 (L~f)`=LeftComp f \/ RightComp f;