:: Functions and Finite Sequences of Real Numbers :: by Jaros{\l}aw Kotowicz :: :: Received March 15, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin registration let f be FinSequence; let x be set ; cluster Coim (f,x) -> finite ; coherence Coim (f,x) is finite ; end; theorem Th1: :: RFINSEQ:1 for f, g, h being FinSequence holds ( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent ) proofend; theorem :: RFINSEQ:2 for f, g being FinSequence holds f ^ g,g ^ f are_fiberwise_equipotent proofend; theorem Th3: :: RFINSEQ:3 for f, g being FinSequence st f,g are_fiberwise_equipotent holds ( len f = len g & dom f = dom g ) proofend; theorem Th4: :: RFINSEQ:4 for f, g being FinSequence holds ( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P ) proofend; defpred S1[ Nat] means for X being finite set for F being Function st card (dom (F | X)) = $1 holds ex a being FinSequence st F | X,a are_fiberwise_equipotent ; Lm1: S1[ 0 ] proofend; Lm2: for n being Element of NAT st S1[n] holds S1[n + 1] proofend; theorem :: RFINSEQ:5 for F being Function for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent proofend; definition let n be Nat; let f be FinSequence; funcf /^ n -> FinSequence means :Def1: :: RFINSEQ:def 1 ( len it = (len f) - n & ( for m being Nat st m in dom it holds it . m = f . (m + n) ) ) if n <= len f otherwise it = {} ; existence ( ( n <= len f implies ex b1 being FinSequence st ( len b1 = (len f) - n & ( for m being Nat st m in dom b1 holds b1 . m = f . (m + n) ) ) ) & ( not n <= len f implies ex b1 being FinSequence st b1 = {} ) ) proofend; uniqueness for b1, b2 being FinSequence holds ( ( n <= len f & len b1 = (len f) - n & ( for m being Nat st m in dom b1 holds b1 . m = f . (m + n) ) & len b2 = (len f) - n & ( for m being Nat st m in dom b2 holds b2 . m = f . (m + n) ) implies b1 = b2 ) & ( not n <= len f & b1 = {} & b2 = {} implies b1 = b2 ) ) proofend; consistency for b1 being FinSequence holds verum ; end; :: deftheorem Def1 defines /^ RFINSEQ:def_1_:_ for n being Nat for f, b3 being FinSequence holds ( ( n <= len f implies ( b3 = f /^ n iff ( len b3 = (len f) - n & ( for m being Nat st m in dom b3 holds b3 . m = f . (m + n) ) ) ) ) & ( not n <= len f implies ( b3 = f /^ n iff b3 = {} ) ) ); definition let D be set ; let n be Nat; let f be FinSequence of D; :: original:/^ redefine funcf /^ n -> FinSequence of D; coherence f /^ n is FinSequence of D proofend; end; Lm3: for n being Nat for D being non empty set for f being FinSequence of D st len f <= n holds f | n = f proofend; theorem Th6: :: RFINSEQ:6 for D being non empty set for f being FinSequence of D for n, m being Nat st n in dom f & m in Seg n holds ( (f | n) . m = f . m & m in dom f ) proofend; theorem Th7: :: RFINSEQ:7 for D being non empty set for f being FinSequence of D for n being Nat for x being set st len f = n + 1 & x = f . (n + 1) holds f = (f | n) ^ <*x*> proofend; theorem Th8: :: RFINSEQ:8 for D being non empty set for f being FinSequence of D for n being Nat holds (f | n) ^ (f /^ n) = f proofend; theorem :: RFINSEQ:9 for R1, R2 being FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds Sum R1 = Sum R2 proofend; definition let R be FinSequence of REAL ; func MIM R -> FinSequence of REAL means :Def2: :: RFINSEQ:def 2 ( len it = len R & it . (len it) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len it) - 1 holds it . n = (R . n) - (R . (n + 1)) ) ); existence ex b1 being FinSequence of REAL st ( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds b1 . n = (R . n) - (R . (n + 1)) ) ) proofend; uniqueness for b1, b2 being FinSequence of REAL st len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds b1 . n = (R . n) - (R . (n + 1)) ) & len b2 = len R & b2 . (len b2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b2) - 1 holds b2 . n = (R . n) - (R . (n + 1)) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines MIM RFINSEQ:def_2_:_ for R, b2 being FinSequence of REAL holds ( b2 = MIM R iff ( len b2 = len R & b2 . (len b2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b2) - 1 holds b2 . n = (R . n) - (R . (n + 1)) ) ) ); theorem Th10: :: RFINSEQ:10 for R being FinSequence of REAL for r being Real for n being Element of NAT st len R = n + 2 & R . (n + 1) = r holds MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*> proofend; theorem Th11: :: RFINSEQ:11 for R being FinSequence of REAL for r, s being Real for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds MIM R = ((MIM R) | n) ^ <*(r - s),s*> proofend; theorem Th12: :: RFINSEQ:12 MIM (<*> REAL) = <*> REAL proofend; theorem Th13: :: RFINSEQ:13 for r being Real holds MIM <*r*> = <*r*> proofend; theorem :: RFINSEQ:14 for r, s being Real holds MIM <*r,s*> = <*(r - s),s*> proofend; theorem :: RFINSEQ:15 for R being FinSequence of REAL for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n) proofend; theorem Th16: :: RFINSEQ:16 for R being FinSequence of REAL st len R <> 0 holds Sum (MIM R) = R . 1 proofend; theorem :: RFINSEQ:17 for R being FinSequence of REAL for n being Element of NAT st n < len R holds Sum (MIM (R /^ n)) = R . (n + 1) proofend; definition let IT be FinSequence of REAL ; redefine attr IT is non-increasing means :Def3: :: RFINSEQ:def 3 for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1); compatibility ( IT is non-increasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ) proofend; end; :: deftheorem Def3 defines non-increasing RFINSEQ:def_3_:_ for IT being FinSequence of REAL holds ( IT is non-increasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ); registration cluster Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing for FinSequence of REAL ; existence ex b1 being FinSequence of REAL st b1 is non-increasing proofend; end; theorem Th18: :: RFINSEQ:18 for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds R is non-increasing proofend; theorem Th19: :: RFINSEQ:19 for R being FinSequence of REAL holds ( R is non-increasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ) proofend; theorem Th20: :: RFINSEQ:20 for R being non-increasing FinSequence of REAL for n being Element of NAT holds R | n is non-increasing FinSequence of REAL proofend; theorem :: RFINSEQ:21 for R being non-increasing FinSequence of REAL for n being Element of NAT holds R /^ n is non-increasing proofend; Lm4: for f, g being non-increasing FinSequence of REAL for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) proofend; defpred S2[ Nat] means for R being FinSequence of REAL st $1 = len R holds ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ; Lm5: S2[ 0 ] proofend; Lm6: for n being Element of NAT st S2[n] holds S2[n + 1] proofend; theorem Th22: :: RFINSEQ:22 for R being FinSequence of REAL ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent proofend; Lm7: for n being Element of NAT for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2 proofend; theorem :: RFINSEQ:23 for R1, R2 being non-increasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds R1 = R2 proofend; theorem :: RFINSEQ:24 for R being FinSequence of REAL for r, s being Real st r <> 0 holds R " {(s / r)} = (r * R) " {s} proofend; theorem :: RFINSEQ:25 for R being FinSequence of REAL holds (0 * R) " {0} = dom R proofend; begin theorem :: RFINSEQ:26 for f, g being Function st rng f = rng g & f is one-to-one & g is one-to-one holds f,g are_fiberwise_equipotent proofend; :: from REVROT_1, 2007.03.18, A.T. theorem :: RFINSEQ:27 for D being set for f being FinSequence of D holds f /^ (len f) = {} proofend; :: from SCMBSORT, 2007.07.26, A.T. theorem :: RFINSEQ:28 for f, g being Function for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds f . k = g . k ) holds f,g are_fiberwise_equipotent proofend; :: form BINARITH, 2008.08.20, A.T. theorem :: RFINSEQ:29 for D being non empty set for f being FinSequence of D for k being Nat holds len (f /^ k) = (len f) -' k proofend; :: from SCPQSORT, 2008.10.12, A.T. theorem Th30: :: RFINSEQ:30 for f, g being FinSequence for x being set st x in dom g & f,g are_fiberwise_equipotent holds ex y being set st ( y in dom g & f . x = g . y ) proofend; theorem Th31: :: RFINSEQ:31 for f, g, h being FinSequence holds ( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent ) proofend; theorem :: RFINSEQ:32 for f, g being FinSequence for m, n, j being Element of NAT st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds f . i = g . i ) & m < j & j <= n holds ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) proofend; theorem :: RFINSEQ:33 for t being FinSequence of INT ex u being FinSequence of REAL st ( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing ) proofend;