:: Subsequences of Almost, Weakly and Poorly One-to-one Finite Sequences :: by Robert Milewski :: :: Received February 1, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin theorem Th1: :: JORDAN23:1 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds len (L_Cut (f,p)) >= 1 proofend; theorem :: JORDAN23:2 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) holds len (R_Cut (f,p)) >= 1 proofend; theorem Th3: :: JORDAN23:3 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) holds B_Cut (f,p,q) <> {} proofend; registration let x be set ; cluster<*x*> -> one-to-one ; coherence <*x*> is one-to-one by FINSEQ_3:93; end; definition let f be FinSequence; attrf is almost-one-to-one means :Def1: :: JORDAN23:def 1 for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j holds i = j; end; :: deftheorem Def1 defines almost-one-to-one JORDAN23:def_1_:_ for f being FinSequence holds ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j holds i = j ); definition let f be FinSequence; attrf is weakly-one-to-one means :Def2: :: JORDAN23:def 2 for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1); end; :: deftheorem Def2 defines weakly-one-to-one JORDAN23:def_2_:_ for f being FinSequence holds ( f is weakly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) ); definition let f be FinSequence; attrf is poorly-one-to-one means :Def3: :: JORDAN23:def 3 for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) if len f <> 2 otherwise verum; consistency verum ; end; :: deftheorem Def3 defines poorly-one-to-one JORDAN23:def_3_:_ for f being FinSequence holds ( ( len f <> 2 implies ( f is poorly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) ) ) & ( not len f <> 2 implies ( f is poorly-one-to-one iff verum ) ) ); theorem :: JORDAN23:4 for D being set for f being FinSequence of D holds ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ) proofend; theorem Th5: :: JORDAN23:5 for D being set for f being FinSequence of D holds ( f is weakly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) proofend; theorem :: JORDAN23:6 for D being set for f being FinSequence of D holds ( f is poorly-one-to-one iff ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ) proofend; registration clusterV13() Function-like one-to-one FinSequence-like -> almost-one-to-one for set ; coherence for b1 being FinSequence st b1 is one-to-one holds b1 is almost-one-to-one proofend; end; registration clusterV13() Function-like FinSequence-like almost-one-to-one -> poorly-one-to-one for set ; coherence for b1 being FinSequence st b1 is almost-one-to-one holds b1 is poorly-one-to-one proofend; end; theorem Th7: :: JORDAN23:7 for f being FinSequence st len f <> 2 holds ( f is weakly-one-to-one iff f is poorly-one-to-one ) proofend; registration cluster empty V13() Function-like FinSequence-like -> weakly-one-to-one for set ; coherence for b1 being FinSequence st b1 is empty holds b1 is weakly-one-to-one proofend; end; registration let x be set ; cluster<*x*> -> weakly-one-to-one ; coherence <*x*> is weakly-one-to-one proofend; end; registration let x, y be set ; cluster<*x,y*> -> poorly-one-to-one ; coherence <*x,y*> is poorly-one-to-one proofend; end; registration cluster non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like weakly-one-to-one for set ; existence ex b1 being FinSequence st ( b1 is weakly-one-to-one & not b1 is empty ) proofend; end; registration let D be non empty set ; cluster non empty V13() V16( NAT ) V17(D) Function-like V26() FinSequence-like FinSubsequence-like circular weakly-one-to-one for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is weakly-one-to-one & b1 is circular & not b1 is empty ) proofend; end; theorem Th8: :: JORDAN23:8 for f being FinSequence st f is almost-one-to-one holds Rev f is almost-one-to-one proofend; theorem Th9: :: JORDAN23:9 for f being FinSequence st f is weakly-one-to-one holds Rev f is weakly-one-to-one proofend; theorem Th10: :: JORDAN23:10 for f being FinSequence st f is poorly-one-to-one holds Rev f is poorly-one-to-one proofend; registration cluster non empty V13() V16( NAT ) Function-like one-to-one V26() FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st ( b1 is one-to-one & not b1 is empty ) proofend; end; registration let f be almost-one-to-one FinSequence; cluster Rev f -> almost-one-to-one ; coherence Rev f is almost-one-to-one by Th8; end; registration let f be weakly-one-to-one FinSequence; cluster Rev f -> weakly-one-to-one ; coherence Rev f is weakly-one-to-one by Th9; end; registration let f be poorly-one-to-one FinSequence; cluster Rev f -> poorly-one-to-one ; coherence Rev f is poorly-one-to-one by Th10; end; theorem Th11: :: JORDAN23:11 for D being non empty set for f being FinSequence of D st f is almost-one-to-one holds for p being Element of D holds Rotate (f,p) is almost-one-to-one proofend; theorem Th12: :: JORDAN23:12 for D being non empty set for f being FinSequence of D st f is weakly-one-to-one & f is circular holds for p being Element of D holds Rotate (f,p) is weakly-one-to-one proofend; theorem Th13: :: JORDAN23:13 for D being non empty set for f being FinSequence of D st f is poorly-one-to-one & f is circular holds for p being Element of D holds Rotate (f,p) is poorly-one-to-one proofend; registration let D be non empty set ; cluster non empty V13() V16( NAT ) V17(D) Function-like one-to-one V26() FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is one-to-one & b1 is circular & not b1 is empty ) proofend; end; registration let D be non empty set ; let f be almost-one-to-one FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> almost-one-to-one ; coherence Rotate (f,p) is almost-one-to-one by Th11; end; registration let D be non empty set ; let f be circular weakly-one-to-one FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> weakly-one-to-one ; coherence Rotate (f,p) is weakly-one-to-one by Th12; end; registration let D be non empty set ; let f be circular poorly-one-to-one FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> poorly-one-to-one ; coherence Rotate (f,p) is poorly-one-to-one by Th13; end; theorem Th14: :: JORDAN23:14 for D being non empty set for f being FinSequence of D holds ( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) ) proofend; registration let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; cluster Cage (C,n) -> almost-one-to-one ; coherence Cage (C,n) is almost-one-to-one proofend; end; registration let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; cluster Cage (C,n) -> weakly-one-to-one ; coherence Cage (C,n) is weakly-one-to-one proofend; end; theorem Th15: :: JORDAN23:15 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f & f is weakly-one-to-one holds B_Cut (f,p,p) = <*p*> proofend; theorem Th16: :: JORDAN23:16 for f being FinSequence st f is one-to-one holds f is weakly-one-to-one proofend; registration clusterV13() Function-like one-to-one FinSequence-like -> weakly-one-to-one for set ; coherence for b1 being FinSequence st b1 is one-to-one holds b1 is weakly-one-to-one by Th16; end; theorem Th17: :: JORDAN23:17 for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) proofend; theorem Th18: :: JORDAN23:18 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i1 being Element of NAT st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds (Index (p,f)) + 1 = i1 proofend; theorem Th19: :: JORDAN23:19 for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. 1 = p proofend; theorem Th20: :: JORDAN23:20 for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q proofend; theorem :: JORDAN23:21 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds L~ (L_Cut (f,p)) c= L~ f proofend; theorem :: JORDAN23:22 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is weakly-one-to-one holds L~ (B_Cut (f,p,q)) c= L~ f proofend; theorem Th23: :: JORDAN23:23 for f, g being FinSequence holds dom f c= dom (f ^' g) proofend; theorem :: JORDAN23:24 for f being non empty FinSequence for g being FinSequence holds dom g c= dom (f ^' g) proofend; theorem Th25: :: JORDAN23:25 for f, g being FinSequence st f ^' g is constant holds f is constant proofend; theorem :: JORDAN23:26 for f, g being FinSequence st f ^' g is constant & f . (len f) = g . 1 & f <> {} holds g is constant proofend; theorem Th27: :: JORDAN23:27 for f being special FinSequence of (TOP-REAL 2) for i, j being Element of NAT holds mid (f,i,j) is special proofend; theorem Th28: :: JORDAN23:28 for f being unfolded FinSequence of (TOP-REAL 2) for i, j being Element of NAT holds mid (f,i,j) is unfolded proofend; theorem Th29: :: JORDAN23:29 for f being FinSequence of (TOP-REAL 2) st f is special holds for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is special proofend; theorem Th30: :: JORDAN23:30 for f being FinSequence of (TOP-REAL 2) st f is special holds for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is special proofend; theorem :: JORDAN23:31 for f being FinSequence of (TOP-REAL 2) st f is special & f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is special proofend; theorem Th32: :: JORDAN23:32 for f being FinSequence of (TOP-REAL 2) st f is unfolded holds for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is unfolded proofend; theorem Th33: :: JORDAN23:33 for f being FinSequence of (TOP-REAL 2) st f is unfolded holds for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is unfolded proofend; theorem :: JORDAN23:34 for f being FinSequence of (TOP-REAL 2) st f is unfolded & f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is unfolded proofend; theorem Th35: :: JORDAN23:35 for f, g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds g is_S-Seq_joining f /. 1,p proofend; theorem Th36: :: JORDAN23:36 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) holds ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f proofend; theorem :: JORDAN23:37 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is weakly-one-to-one & len f >= 2 holds L_Cut (f,(f /. 1)) = f proofend; theorem Th38: :: JORDAN23:38 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) holds L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) proofend; theorem Th39: :: JORDAN23:39 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds R_Cut (f,p) is_S-Seq_joining f /. 1,p proofend; theorem Th40: :: JORDAN23:40 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds L_Cut (f,p) is_S-Seq_joining p,f /. (len f) proofend; theorem :: JORDAN23:41 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds R_Cut (f,p) is being_S-Seq proofend; theorem Th42: :: JORDAN23:42 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds L_Cut (f,p) is being_S-Seq proofend; Lm1: for f being non empty FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) holds B_Cut (f,p,q) is_S-Seq_joining p,q proofend; theorem Th43: :: JORDAN23:43 for f being non empty FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 holds B_Cut (f,p,q) is_S-Seq_joining p,q proofend; theorem :: JORDAN23:44 for f being non empty FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 holds B_Cut (f,p,q) is being_S-Seq proofend; theorem :: JORDAN23:45 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds ex B being S-Sequence_in_R2 st ( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) proofend;