:: by Jaros{\l}aw Kotowicz

::

:: Received March 15, 1993

:: Copyright (c) 1993-2017 Association of Mizar Users

theorem Th1: :: RFINSEQ:1

for f, g, h being FinSequence holds

( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent )

( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent )

proof end;

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 )

( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P )

proof end;

defpred S

for F being Function st card (dom (F | X)) = $1 holds

ex a being FinSequence st F | X,a are_fiberwise_equipotent ;

Lm1: S

proof end;

Lm2: for n being Nat st S

S

proof end;

theorem :: RFINSEQ:5

for F being Function

for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent

for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent

proof end;

definition

let n be Nat;

let f be FinSequence;

( ( n <= len f implies ex b_{1} being FinSequence st

( len b_{1} = (len f) - n & ( for m being Nat st m in dom b_{1} holds

b_{1} . m = f . (m + n) ) ) ) & ( not n <= len f implies ex b_{1} being FinSequence st b_{1} = {} ) )

for b_{1}, b_{2} being FinSequence holds

( ( n <= len f & len b_{1} = (len f) - n & ( for m being Nat st m in dom b_{1} holds

b_{1} . m = f . (m + n) ) & len b_{2} = (len f) - n & ( for m being Nat st m in dom b_{2} holds

b_{2} . m = f . (m + n) ) implies b_{1} = b_{2} ) & ( not n <= len f & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being FinSequence holds verum
;

end;
let f be FinSequence;

func f /^ 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 ( 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 = {} ;

( ( n <= len f implies ex b

( len b

b

proof end;

uniqueness for b

( ( n <= len f & len b

b

b

proof end;

consistency for b

:: deftheorem Def1 defines /^ RFINSEQ:def 1 :

for n being Nat

for f, b_{3} being FinSequence holds

( ( n <= len f implies ( b_{3} = f /^ n iff ( len b_{3} = (len f) - n & ( for m being Nat st m in dom b_{3} holds

b_{3} . m = f . (m + n) ) ) ) ) & ( not n <= len f implies ( b_{3} = f /^ n iff b_{3} = {} ) ) );

for n being Nat

for f, b

( ( n <= len f implies ( b

b

definition

let D be set ;

let n be Nat;

let f be FinSequence of D;

:: original: /^

redefine func f /^ n -> FinSequence of D;

coherence

f /^ n is FinSequence of D

end;
let n be Nat;

let f be FinSequence of D;

:: original: /^

redefine func f /^ n -> FinSequence of D;

coherence

f /^ n is FinSequence of D

proof 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

proof end;

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 )

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 )

proof end;

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*>

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*>

proof end;

definition

let R be real-valued FinSequence;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len R & b_{1} . (len b_{1}) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b_{1}) - 1 holds

b_{1} . n = (R . n) - (R . (n + 1)) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len R & b_{1} . (len b_{1}) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b_{1}) - 1 holds

b_{1} . n = (R . n) - (R . (n + 1)) ) & len b_{2} = len R & b_{2} . (len b_{2}) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b_{2}) - 1 holds

b_{2} . n = (R . n) - (R . (n + 1)) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines MIM RFINSEQ:def 2 :

for R being real-valued FinSequence

for b_{2} being FinSequence of REAL holds

( b_{2} = MIM R iff ( len b_{2} = len R & b_{2} . (len b_{2}) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b_{2}) - 1 holds

b_{2} . n = (R . n) - (R . (n + 1)) ) ) );

for R being real-valued FinSequence

for b

( b

b

theorem Th10: :: RFINSEQ:10

for R being FinSequence of REAL

for r being Real

for n being Nat st len R = n + 2 & R . (n + 1) = r holds

MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>

for r being Real

for n being Nat st len R = n + 2 & R . (n + 1) = r holds

MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>

proof end;

theorem Th11: :: RFINSEQ:11

for R being FinSequence of REAL

for r, s being Real

for n being Nat st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds

MIM R = ((MIM R) | n) ^ <*(r - s),s*>

for r, s being Real

for n being Nat st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds

MIM R = ((MIM R) | n) ^ <*(r - s),s*>

proof end;

definition

let IT be real-valued FinSequence;

( IT is non-increasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) )

end;
redefine attr IT is non-increasing means :Def3: :: RFINSEQ:def 3

for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1);

compatibility for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1);

( IT is non-increasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) )

proof end;

:: deftheorem Def3 defines non-increasing RFINSEQ:def 3 :

for IT being real-valued FinSequence holds

( IT is non-increasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) );

for IT being real-valued FinSequence holds

( IT is non-increasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n >= IT . (n + 1) );

registration

ex b_{1} being FinSequence of REAL st b_{1} is non-increasing
end;

cluster Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued non-increasing for FinSequence of REAL ;

existence ex b

proof end;

theorem Th19: :: RFINSEQ:19

for R being FinSequence of REAL holds

( R is non-increasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds

R . n >= R . m )

( R is non-increasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds

R . n >= R . m )

proof end;

theorem Th20: :: RFINSEQ:20

for R being non-increasing FinSequence of REAL

for n being Nat holds R | n is non-increasing FinSequence of REAL

for n being Nat holds R | n is non-increasing FinSequence of REAL

proof end;

theorem :: RFINSEQ:21

for R being non-increasing FinSequence of REAL

for n being Element of NAT holds R /^ n is non-increasing

for n being Element of NAT holds R /^ n is non-increasing

proof end;

Lm4: for f, g being non-increasing FinSequence of REAL

for n being 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 )

proof end;

defpred S

ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ;

Lm5: S

proof end;

Lm6: for n being Nat st S

S

proof end;

theorem Th22: :: RFINSEQ:22

for R being FinSequence of REAL ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent

proof end;

Lm7: for n being Nat

for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds

g1 = g2

proof end;

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

f,g are_fiberwise_equipotent

proof end;

:: from REVROT_1, 2007.03.18, A.T.

:: 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

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

proof end;

:: 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

for f being FinSequence of D

for k being Nat holds len (f /^ k) = (len f) -' k

proof end;

:: 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 )

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 )

proof end;

theorem Th31: :: RFINSEQ:31

for f, g, h being FinSequence holds

( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )

( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )

proof end;

theorem :: RFINSEQ:32

for f, g being FinSequence

for m, n, j being Nat st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Nat st 1 <= i & i <= m holds

f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds

f . i = g . i ) & m < j & j <= n holds

ex k being Nat st

( m < k & k <= n & f . j = g . k )

for m, n, j being Nat st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Nat st 1 <= i & i <= m holds

f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds

f . i = g . i ) & m < j & j <= n holds

ex k being Nat st

( m < k & k <= n & f . j = g . k )

proof end;

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 )

( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )

proof end;