:: On the components of the complement of a special polygonal curve :: by Andrzej Trybulec and Yatsuka Nakamura :: :: Received January 21, 1999 :: Copyright (c) 1999-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, SPPOL_2, RCOMP_1, EUCLID, TOPREAL1, XBOOLE_0, PARTFUN1, JORDAN3, JORDAN5C, FINSEQ_1, XXREAL_0, ARYTM_3, GROUP_2, RELAT_1, TARSKI, PRE_TOPC, FUNCT_1, ARYTM_1, RLTOPSP1, ORDINAL4, SPRECT_2, GOBOARD5, PSCOMP_1, GOBOARD9, SPRECT_1, GOBOARD2, TREES_1, MATRIX_1, TOPS_1, MCART_1, TOPREAL4, SPPOL_1, FINSEQ_5, FINSEQ_4, FINSEQ_6, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4, FINSEQ_5, FINSEQ_6, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9, JORDAN3, PSCOMP_1, JORDAN5C, SPRECT_1, SPRECT_2, XXREAL_0; constructors REAL_1, FINSEQ_4, TOPS_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL4, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1, SPRECT_2, GOBOARD1, NAT_D, MATRIX_1; registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1, TOPREAL1, GOBOARD2, SPPOL_2, GOBOARD9, SPRECT_1, SPRECT_3, REVROT_1, FUNCT_1, EUCLID, ZFMISC_1, XREAL_0, NAT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve i,j,l for Nat; theorem :: SPRECT_4:1 for f being S-Sequence_in_R2, Q being closed Subset of TOP-REAL 2 st L~f meets Q & not f/.1 in Q holds L~R_Cut(f,First_Point(L~f,f/.1,f/.len f,Q) ) /\ Q = { First_Point(L~f,f/.1,f/.len f,Q) }; theorem :: SPRECT_4:2 for f being non empty FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p = f/.len f holds L~L_Cut (f,p) = {}; theorem :: SPRECT_4:3 for f being S-Sequence_in_R2, p being Point of TOP-REAL 2, j st 1 <=j & j < len f & p in L~mid(f,j,len f) holds LE f/.j, p, L~f, f/.1, f/.len f ; theorem :: SPRECT_4:4 for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2, j st 1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(p,f/.(j+1)) holds LE p, q, L~f, f/.1, f/.len f; theorem :: SPRECT_4:5 for f being S-Sequence_in_R2, Q being closed Subset of TOP-REAL 2 st L~f meets Q & not f/.len f in Q holds L~L_Cut(f,Last_Point(L~f,f/.1,f/.len f ,Q)) /\ Q = { Last_Point(L~f,f/.1,f/.len f,Q) }; reserve q for Point of TOP-REAL 2; theorem :: SPRECT_4:6 for f being non constant standard special_circular_sequence holds LeftComp f <> RightComp f;