:: Subsequences of Standard Special Circular Sequences in $ { \cal E :: } ^2_ { \rm T } $ :: by Yatsuka Nakamura , Roman Matuszewski and Adam Grabowski :: :: Received May 12, 1997 :: Copyright (c) 1997-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, NAT_1, ARYTM_3, INT_1, CARD_1, ARYTM_1, XXREAL_0, RELAT_1, XBOOLE_0, FINSEQ_1, FINSEQ_6, FUNCT_1, PARTFUN1, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, FINSEQ_5, RLTOPSP1, GOBOARD5, ORDINAL4, TARSKI, PRE_TOPC, SUPINF_2, TOPREAL4, TOPREAL2, MCART_1, JORDAN4; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_5, STRUCT_0, TOPREAL1, TOPREAL2, TOPREAL4, GOBOARD5, PRE_TOPC, RLVECT_1, RLTOPSP1, EUCLID, FINSEQ_6, RFINSEQ, XXREAL_0; constructors REAL_1, NAT_D, RFINSEQ, BINARITH, FINSEQ_5, TOPREAL2, TOPREAL4, GOBOARD5, RELSET_1; registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, EUCLID, SPPOL_2, GOBOARD5, NAT_1, CARD_1, ORDINAL1, FINSEQ_5; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve i, i1, i2, j, k for Nat, r, s for Real; theorem :: JORDAN4:1 for i, j being Nat holds j0; theorem :: JORDAN4:2 for i,j being Nat holds j<=i & i & len mid(f1,k,k)=1; theorem :: JORDAN4:16 for f1 being FinSequence holds mid(f1,0,0)=f1|1; registration cluster empty for FinSequence; end; registration let f be empty FinSequence; let k be Nat; cluster f|k -> empty; end; theorem :: JORDAN4:17 for f1 being FinSequence st len f1 Nat equals :: JORDAN4:def 1 (n mod (len f -'1)) if n mod (len f -'1)<>0 otherwise len f -'1; end; theorem :: JORDAN4:21 for f being FinSequence holds S_Drop(len f-'1,f)=len f-'1; theorem :: JORDAN4:22 for n being Nat, f being FinSequence st 1<=n & n<=len f-'1 holds S_Drop(n,f)=n; theorem :: JORDAN4:23 for n being Nat,f being FinSequence holds S_Drop(n,f) =S_Drop(n+(len f-'1),f) & S_Drop(n,f)=S_Drop(len f-'1+n,f); definition let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Nat; pred g is_a_part>_of f,i1,i2 means :: JORDAN4:def 2 1<=i1 & i1+1<=len f & 1<=i2 & i2+1 <=len f & g.len g=f.i2 & 1<=len g & len g_of f,i1,i2 or g is_a_part<_of f,i1,i2; end; theorem :: JORDAN4:24 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part_of f,i1,i2 holds 1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g_of f ,i1,i2 & i1<=i2 holds len g=i2-'i1+1 & g=mid(f,i1,i2); theorem :: JORDAN4:26 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part>_of f ,i1,i2 & i1>i2 holds len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2) & g=mid(f ,i1,len f-'1)^mid(f,1,i2); theorem :: JORDAN4:27 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part<_of f ,i1,i2 & i1>=i2 holds len g=i1-'i2+1 & g=mid(f,i1,i2); theorem :: JORDAN4:28 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part<_of f ,i1,i2 & i1_of f ,i1,i2 holds Rev g is_a_part<_of f,i2,i1; theorem :: JORDAN4:30 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part<_of f ,i1,i2 holds Rev g is_a_part>_of f,i2,i1; theorem :: JORDAN4:31 for f being non constant standard special_circular_sequence, i1, i2 being Nat st 1<=i1 & i1<=i2 & i2_of f,i1,i2; theorem :: JORDAN4:32 for f being non constant standard special_circular_sequence, i1, i2 being Nat st 1<=i1 & i1<=i2 & i2i2 & i1_of f,i1,i2; theorem :: JORDAN4:34 for f being non constant standard special_circular_sequence, i1, i2 being Nat st 1<=i1 & i1p0 holds q1 in LSeg(p,q2) or q2 in LSeg(p,q1); theorem :: JORDAN4:42 for f being non constant standard special_circular_sequence holds LSeg(f,1)/\ LSeg(f,len f-'1)={f.1}; theorem :: JORDAN4:43 for f being non constant standard special_circular_sequence, i1, i2 being Nat,g1,g2 being FinSequence of TOP-REAL 2 st 1<=i1 & i1_of f ,i1,i2 & i1i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2; theorem :: JORDAN4:46 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part>_of f ,i1,i2 & i1<>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2; theorem :: JORDAN4:47 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part<_of f ,i1,i2 & i1<>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2; theorem :: JORDAN4:48 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part_of f, i1,i2 & i1<>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2; theorem :: JORDAN4:49 for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part_of f,i1,i2 & g.1<>g.len g holds L~g is_S-P_arc_joining f/.i1,f/.i2; theorem :: JORDAN4:50 for f being non constant standard special_circular_sequence, i1, i2 being Nat st 1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & i1<>i2 ex g1,g2 being FinSequence of TOP-REAL 2 st g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f & L~g1 is_S-P_arc_joining f/.i1,f/.i2 & L~g2 is_S-P_arc_joining f/.i1,f/.i2 & for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds g=g1 or g=g2; reserve g, g1, g2 for FinSequence of TOP-REAL 2; theorem :: JORDAN4:51 for f being non constant standard special_circular_sequence, P being non empty Subset of TOP-REAL 2 st P = L~f holds P is being_simple_closed_curve; theorem :: JORDAN4:52 for f being non constant standard special_circular_sequence, g1, g2 st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2 holds g1=g2; theorem :: JORDAN4:53 for f being non constant standard special_circular_sequence, g1, g2 st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds g1=g2; theorem :: JORDAN4:54 for f being non constant standard special_circular_sequence, g1, g2 st i1<>i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds g1.2<> g2.2; theorem :: JORDAN4:55 for f being non constant standard special_circular_sequence, g1, g2 st i1<>i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1.2=g2.2 holds g1=g2; definition let f be non constant standard special_circular_sequence, i1,i2 be Element of NAT; assume that 1<=i1 and i1+1<=len f and 1<=i2 and i2+1<=len f and i1<>i2; func Lower (f,i1,i2) -> FinSequence of TOP-REAL 2 means :: JORDAN4:def 5 it is_a_part_of f,i1 ,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2 implies it.2=f.(i1+1) )& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2 implies it.2=f.S_Drop( i1-'1,f)); func Upper (f,i1,i2) -> FinSequence of TOP-REAL 2 means :: JORDAN4:def 6 it is_a_part_of f,i1 ,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2 implies it.2=f.(i1+1) )& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2 implies it.2=f.S_Drop( i1-'1,f)); end;