:: Functions and Finite Sequences of Real Numbers
::  by Jaros{\l}aw Kotowicz
::
:: Received March 15, 1993
:: Copyright (c) 1993-2012 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, NUMBERS, RELAT_1, FUNCT_1,
      RELSET_1, FUNCT_2, FINSEQ_1, XCMPLX_0, XREAL_0, ORDINAL1, NAT_1, REAL_1,
      SEQ_1, CLASSES1, SEQM_3, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_4, RVSUM_1,
      XXREAL_0;
 constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, BINOP_2, SEQM_3,
      FINSEQ_4, FINSOP_1, RVSUM_1, SEQ_1, FUNCOP_1, CLASSES1, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XREAL_0, NAT_1,
      MEMBERED, FINSEQ_1, FUNCOP_1, VALUED_0, CARD_1, INT_1, RELSET_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve x,y for set,
  n,m for Element of NAT,
  r,s for Real;

registration
  let f be FinSequence, x be set;
  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 FinSequence of REAL;
  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 Element of 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 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 *>;

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 Element of 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 Element of NAT st n<len R holds Sum
  MIM(R/^n) = R.(n+1);

definition
  let IT be FinSequence of REAL;
  redefine attr IT is non-increasing means
:: RFINSEQ:def 3

  for n be Element of NAT st n in dom IT & n+1 in dom IT holds
  IT.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 Element of NAT st n in dom R & m in dom R & n<m holds R.n>=R.m;

theorem :: RFINSEQ:20
  for R be non-increasing FinSequence of REAL, n be Element of NAT
  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 be Real 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 D being set, f being FinSequence of D 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 D being non empty set, f being FinSequence of D, 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 Element of NAT st f,g
are_fiberwise_equipotent & m<=n & n <= len f & (for i be Element of NAT st 1<=i
& i<=m holds f.i=g.i) & (for i be Element of NAT st n<i & i<=len f holds f.i=g.
  i) & m<j & j<=n holds ex k be Element of NAT st m<k & k<=n & f.j=g.k;

theorem :: RFINSEQ:33
  for t being FinSequence of INT holds ex u being FinSequence of REAL
  st t,u are_fiberwise_equipotent & u is FinSequence of INT
  & u is non-increasing;