:: Functions and Finite Sequences of Real Numbers :: by Jaros{\l}aw Kotowicz :: :: Received March 15, 1993 :: Copyright (c) 1993-2018 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, FINSEQ_1, RELAT_1, FINSET_1, CLASSES1, ORDINAL4, CARD_1, ARYTM_3, FUNCT_2, XBOOLE_0, TARSKI, NAT_1, FUNCT_1, ARYTM_1, XXREAL_0, CARD_3, VALUED_0, FUNCOP_1, FUNCT_4, RFINSEQ; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, XCMPLX_0, XREAL_0, NAT_1, REAL_1, CLASSES1, SEQM_3, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_4, VALUED_0, RVSUM_1, XXREAL_0; constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, BINOP_2, SEQM_3, FINSEQ_4, FINSOP_1, RVSUM_1, FUNCOP_1, CLASSES1, RELSET_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, FINSEQ_1, FUNCOP_1, VALUED_0, CARD_1, INT_1, RELSET_1, RVSUM_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x,y for set, n,m for Nat, r,s for Real; registration let f be finite Relation, x be object; cluster Coim(f,x) -> finite; end; theorem :: RFINSEQ:1 for f,g,h be FinSequence holds f,g are_fiberwise_equipotent iff f^h, g^h are_fiberwise_equipotent; theorem :: RFINSEQ:2 for f,g be FinSequence holds f^g, g^f are_fiberwise_equipotent; theorem :: RFINSEQ:3 for f,g be FinSequence st f,g are_fiberwise_equipotent holds len f = len g & dom f = dom g; theorem :: RFINSEQ:4 for f,g be FinSequence holds f,g are_fiberwise_equipotent iff ex P be Permutation of dom g st f = g*P; theorem :: RFINSEQ:5 for F be Function, X be finite set ex f be FinSequence st F|X, f are_fiberwise_equipotent; definition let n be Nat, f be FinSequence; func f /^ n -> FinSequence means :: RFINSEQ:def 1 len it = len f - n & for m be Nat st m in dom it holds it.m = f.(m+n) if n<=len f otherwise it = {}; end; definition let D be set, n be Nat, f be FinSequence of D; redefine func f /^ n -> FinSequence of D; end; theorem :: RFINSEQ:6 for D be non empty set, f be FinSequence of D, n,m be Nat holds n in dom f & m in Seg n implies (f|n).m = f.m & m in dom f; theorem :: RFINSEQ:7 for D be non empty set, f be FinSequence of D, n be Nat, x be set st len f = n+1 & x = f.(n+1) holds f = (f|n) ^ <*x*>; theorem :: RFINSEQ:8 for D be non empty set, f be FinSequence of D, n be Nat holds (f|n)^(f/^n) = f; theorem :: RFINSEQ:9 for R1,R2 be FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds Sum R1 = Sum R2; definition let R be real-valued FinSequence; func MIM(R) -> FinSequence of REAL means :: RFINSEQ:def 2 len it = len R & it.(len it) = R.(len R) & for n be Nat st 1 <= n & n <= len it - 1 holds it.n = (R.n) - (R.(n+1)); end; theorem :: RFINSEQ:10 for R be FinSequence of REAL, r be Real, n be Nat st len R = n+2 & R.(n+1) = r holds MIM(R|(n+1)) = MIM(R)|n ^ <* r *>; theorem :: RFINSEQ:11 for R be FinSequence of REAL, r,s be Real, n be Nat st len R = n+2 & R.(n+1) = r & R.(n+2) = s holds MIM(R) = MIM(R)|n ^ <* r-s,s *>; theorem :: RFINSEQ:12 MIM( <*>REAL ) = <*>REAL; theorem :: RFINSEQ:13 for r be Real holds MIM(<*r*>) = <*r*>; theorem :: RFINSEQ:14 for r,s be Real holds MIM(<*r,s*>) = <*r-s,s*>; theorem :: RFINSEQ:15 for R be FinSequence of REAL, n be Nat holds MIM(R) /^ n = MIM(R/^n); theorem :: RFINSEQ:16 for R be FinSequence of REAL st len R <> 0 holds Sum MIM(R) = R. 1; theorem :: RFINSEQ:17 for R be FinSequence of REAL, n be Nat st n= IT.(n+1); end; registration cluster non-increasing for FinSequence of REAL; end; theorem :: RFINSEQ:18 for R be FinSequence of REAL st len R = 0 or len R = 1 holds R is non-increasing; theorem :: RFINSEQ:19 for R be FinSequence of REAL holds R is non-increasing iff for n,m be Nat st n in dom R & m in dom R & n=R.m; theorem :: RFINSEQ:20 for R be non-increasing FinSequence of REAL, n holds R|n is non-increasing FinSequence of REAL; theorem :: RFINSEQ:21 for R be non-increasing FinSequence of REAL, n be Element of NAT holds R /^ n is non-increasing; theorem :: RFINSEQ:22 for R be FinSequence of REAL ex R1 be non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent; theorem :: RFINSEQ:23 for R1,R2 be non-increasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds R1 = R2; theorem :: RFINSEQ:24 for R be FinSequence of REAL, r,s st r <> 0 holds R"{s/r} = (r *R)"{ s }; theorem :: RFINSEQ:25 for R be FinSequence of REAL holds (0*R)"{0} = dom R; begin :: Addenda :: from VECTSP_9, 2006.01.06, A.T. reserve f, g for Function; theorem :: RFINSEQ:26 for f, g st rng f = rng g & f is one-to-one & g is one-to-one holds f,g are_fiberwise_equipotent; :: from REVROT_1, 2007.03.18, A.T. theorem :: RFINSEQ:27 for f being FinSequence holds f /^ len f = {}; :: from SCMBSORT, 2007.07.26, A.T. theorem :: RFINSEQ:28 for f,g be Function,m,n be set st f.m=g.n & f.n=g.m & m in dom f & n in dom f & dom f = dom g & (for k be set st k<>m & k<>n & k in dom f holds f.k= g.k) holds f,g are_fiberwise_equipotent; :: form BINARITH, 2008.08.20, A.T. theorem :: RFINSEQ:29 for f being FinSequence, k being Nat holds len (f/^k)=len f-'k; :: from SCPQSORT, 2008.10.12, A.T. theorem :: RFINSEQ:30 :: RFINSEQ:17 for f,g be FinSequence,x be set st x in dom g & f,g are_fiberwise_equipotent holds ex y be set st y in dom g & f.x=g.y; theorem :: RFINSEQ:31 for f,g,h be FinSequence holds f,g are_fiberwise_equipotent iff h^f, h^g are_fiberwise_equipotent; theorem :: RFINSEQ:32 for f,g be FinSequence,m,n,j be Nat st f,g are_fiberwise_equipotent & m<=n & n <= len f & (for i be Nat st 1<=i & i<=m holds f.i=g.i) & (for i be Nat st n