:: Some properties of special polygonal curves :: by Andrzej Trybulec and Yatsuka Nakamura :: :: Received October 22, 1998 :: Copyright (c) 1998-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, NAT_1, XBOOLE_0, FINSEQ_1, ORDINAL4, PARTFUN1, XXREAL_0, ARYTM_3, MATRIX_1, ZFMISC_1, SUBSET_1, PRE_TOPC, EUCLID, REAL_1, CARD_1, ARYTM_1, RELAT_1, SUPINF_2, RLTOPSP1, METRIC_1, RELAT_2, CONVEX1, RCOMP_1, CONNSP_1, TARSKI, PCOMPS_1, SPPOL_1, MCART_1, GOBOARD1, TREES_1, PSCOMP_1, TOPREAL1, SPRECT_1, SPPOL_2, JORDAN3, FUNCT_1, RFINSEQ, GROUP_2, GOBOARD5, GOBOARD9, TOPREAL4, JORDAN5D, GOBOARD2, SPRECT_2, COMPLEX1, ORDINAL2, TOPS_1, JORDAN5C, FINSEQ_5; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, NAT_D, CARD_1, RFINSEQ, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, MATRIX_1, SEQM_3, SEQ_4, FINSEQ_6, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4, PSCOMP_1, GOBOARD1, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9, JORDAN3, JORDAN5C, JORDAN5D, SPRECT_1, SPRECT_2, XXREAL_0; constructors REAL_1, FINSEQ_4, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, TOPS_2, COMPTS_1, MATRIX_1, TOPMETR, TOPREAL2, TOPREAL4, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1, SPRECT_2, JORDAN5D, GOBOARD1, PCOMPS_1, BINARITH, FUNCSDOM, CONVEX1, SEQ_4, RVSUM_1, VALUED_0; registrations RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, SPPOL_2, SPRECT_1, SPRECT_2, VALUED_0, CARD_1, FUNCT_1, SEQ_4, SPPOL_1, TOPS_1, JORDAN1, RVSUM_1, NAT_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries theorem :: SPRECT_3:1 for D being non empty set for f being non empty FinSequence of D, g being FinSequence of D holds (g^f)/.len(g^f) = f/.len f; theorem :: SPRECT_3:2 for a,b,c,d being set holds Indices (a,b)][(c,d) = {[1,1],[1,2], [2,1],[2,2]} ; begin :: Euclidean Space reserve i,j,k,n,m for Nat; theorem :: SPRECT_3:3 for p,q being Point of TOP-REAL n, r being Real st 0 < r & p = ( 1-r)*p+r*q holds p = q; theorem :: SPRECT_3:4 for p,q being Point of TOP-REAL n, r being Real st r < 1 & p = ( 1-r)*q+r*p holds p = q; theorem :: SPRECT_3:5 for p,q being Point of TOP-REAL n st p = 1/2*(p+q) holds p = q; theorem :: SPRECT_3:6 for p,q,r being Point of TOP-REAL n st q in LSeg(p,r) & r in LSeg(p,q) holds q = r; begin :: Euclidean Plane theorem :: SPRECT_3:7 for A being non empty Subset of TOP-REAL 2, p being Element of Euclid 2, r being Real st A = Ball(p,r) holds A is connected; theorem :: SPRECT_3:8 for A, B being Subset of TOP-REAL 2 st A is open & B is_a_component_of A holds B is open; theorem :: SPRECT_3:9 for p,q,r,s being Point of TOP-REAL 2 st LSeg(p,q) is horizontal & LSeg(r,s) is horizontal & LSeg(p,q) meets LSeg(r,s) holds p`2= r`2; theorem :: SPRECT_3:10 for p,q,r being Point of TOP-REAL 2 st LSeg(p,q) is vertical & LSeg(q, r) is horizontal holds LSeg(p,q) /\ LSeg(q,r) = {q}; theorem :: SPRECT_3:11 for p,q,r,s being Point of TOP-REAL 2 st LSeg(p,q) is horizontal & LSeg(s,r) is vertical & r in LSeg(p,q) holds LSeg(p,q) /\ LSeg(s,r) = {r}; begin :: Main reserve p,q for Point of TOP-REAL 2; reserve G for Go-board; theorem :: SPRECT_3:12 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G implies G*(i,j)`2 <= G*(i,k)`2; theorem :: SPRECT_3:13 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G implies G*(i,j)`1 <= G*(k,j)`1; reserve C for Subset of TOP-REAL 2; theorem :: SPRECT_3:14 LSeg(NW-corner C,NE-corner C) c= L~SpStSeq C; theorem :: SPRECT_3:15 for C being non empty compact Subset of TOP-REAL 2 holds N-min C in LSeg(NW-corner C,NE-corner C); registration let C; cluster LSeg(NW-corner C,NE-corner C) -> horizontal; end; theorem :: SPRECT_3:16 for g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st g/.1 <> p & ((g/.1)`1 = p`1 or (g/.1)`2 = p`2) & g is being_S-Seq & LSeg(p,g/.1 ) /\ L~g={ g/.1 } holds <*p*>^g is being_S-Seq; theorem :: SPRECT_3:17 for f being S-Sequence_in_R2, p being Point of TOP-REAL 2 st 1 non vertical non horizontal; cluster LeftComp f -> being_Region; cluster RightComp f -> being_Region; end; theorem :: SPRECT_3:25 for f being non constant standard special_circular_sequence holds RightComp f misses L~f; theorem :: SPRECT_3:26 for f being non constant standard special_circular_sequence holds LeftComp f misses L~f; theorem :: SPRECT_3:27 for f being non constant standard special_circular_sequence holds i_w_n f < i_e_n f; theorem :: SPRECT_3:28 for f being non constant standard special_circular_sequence ex i st 1 <= i & i < len GoB f & N-min L~f = (GoB f)*(i,width GoB f); theorem :: SPRECT_3:29 for f being clockwise_oriented non constant standard special_circular_sequence st i in dom GoB f & f/.1 = (GoB f)*(i,width GoB f) & f/.1 = N-min L~f holds f/.2 = (GoB f)*(i+1,width GoB f) & f/.(len f -' 1) = ( GoB f)*(i,width GoB f -' 1); theorem :: SPRECT_3:30 for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f/.1 in L~mid(f,i,j) holds i = 1 or j = len f; theorem :: SPRECT_3:31 for f being clockwise_oriented non constant standard special_circular_sequence st f/.1 = N-min L~f holds LSeg(f/.1,f/.2) c= L~ SpStSeq L~f; begin :: Rectangular theorem :: SPRECT_3:32 for f being rectangular FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f holds p`1 = W-bound L~f or p`1 = E-bound L~f or p`2 = S-bound L~f or p`2 = N-bound L~f; registration cluster rectangular for special_circular_sequence; end; theorem :: SPRECT_3:33 for f being rectangular special_circular_sequence, g being S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds L~f meets L~g; theorem :: SPRECT_3:34 for f being rectangular special_circular_sequence holds SpStSeq L~f = f; theorem :: SPRECT_3:35 for f being rectangular special_circular_sequence holds L~f = { p where p is Point of TOP-REAL 2: p`1 = W-bound L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f or p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = N-bound L~f or p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = S-bound L~f or p`1 = E-bound L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f}; theorem :: SPRECT_3:36 for f being rectangular special_circular_sequence holds GoB f = (f/.4,f/.1)][(f/.3,f/.2); theorem :: SPRECT_3:37 for f being rectangular special_circular_sequence holds LeftComp f = {p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f & S-bound L~f <= p`2 & p`2 <= N-bound L~f)} & RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f & S-bound L~f < q`2 & q`2 < N-bound L~f}; registration cluster clockwise_oriented for rectangular special_circular_sequence; end; registration cluster -> clockwise_oriented for rectangular special_circular_sequence; end; theorem :: SPRECT_3:38 for f being rectangular special_circular_sequence, g being S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds Last_Point(L~g,g/.1,g/.len g,L~f) <> NW-corner L~f; theorem :: SPRECT_3:39 for f being rectangular special_circular_sequence, g being S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds Last_Point(L~g,g/.1,g/.len g,L~f) <> SE-corner L~f; theorem :: SPRECT_3:40 for f being rectangular special_circular_sequence, p being Point of TOP-REAL 2 st W-bound L~f > p`1 or p`1 > E-bound L~f or S-bound L~f > p`2 or p`2 > N-bound L~f holds p in LeftComp f; theorem :: SPRECT_3:41 for f being clockwise_oriented non constant standard special_circular_sequence st f/.1 = N-min L~f holds LeftComp SpStSeq L~f c= LeftComp f; begin :: In the area theorem :: SPRECT_3:42 for f being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 holds <*p,q*> is_in_the_area_of f iff <*p*> is_in_the_area_of f & <* q*> is_in_the_area_of f; theorem :: SPRECT_3:43 for f being rectangular FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st <*p*> is_in_the_area_of f & (p`1 = W-bound L~f or p`1 = E-bound L~f or p`2 = S-bound L~f or p`2 = N-bound L~f) holds p in L~f; theorem :: SPRECT_3:44 for f being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2, r being Real st 0<=r & r <= 1 & <*p,q*> is_in_the_area_of f holds <*(1-r)*p+r*q*> is_in_the_area_of f; theorem :: SPRECT_3:45 for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of f & i in dom g holds <*g/.i*> is_in_the_area_of f; theorem :: SPRECT_3:46 for f, g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st g is_in_the_area_of f & p in L~g holds <*p*> is_in_the_area_of f; theorem :: SPRECT_3:47 for f being rectangular FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 st not q in L~f & <*p,q*> is_in_the_area_of f holds LSeg(p, q) /\ L~f c= {p}; theorem :: SPRECT_3:48 for f being rectangular FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 st p in L~f & not q in L~f & <*q*> is_in_the_area_of f holds LSeg(p, q) /\ L~f = {p}; theorem :: SPRECT_3:49 for f being non constant standard special_circular_sequence st 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f holds <*(GoB f)*(i,j)*> is_in_the_area_of f; theorem :: SPRECT_3:50 for g being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 st <*p,q*> is_in_the_area_of g holds <*1/2*(p+q)*> is_in_the_area_of g; theorem :: SPRECT_3:51 for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of f holds Rev g is_in_the_area_of f; theorem :: SPRECT_3:52 for f, g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~g holds R_Cut(g,p) is_in_the_area_of f; theorem :: SPRECT_3:53 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL2 holds g is_in_the_area_of f iff g is_in_the_area_of SpStSeq L~f; theorem :: SPRECT_3:54 for f being rectangular special_circular_sequence, g being S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds L_Cut(g, Last_Point(L~g,g/.1,g/.len g,L~f)) is_in_the_area_of f; theorem :: SPRECT_3:55 for f being non constant standard special_circular_sequence st 1 <= i & i < len GoB f & 1 <= j & j < width GoB f holds Int cell(GoB f,i,j) misses L~ SpStSeq L~f; theorem :: SPRECT_3:56 for f, g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~g holds L_Cut(g,p) is_in_the_area_of f;