:: Functions and Finite Sequences of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received March 15, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users

begin

theorem :: RFINSEQ:1

canceled;

theorem :: RFINSEQ:2

canceled;

theorem :: RFINSEQ:3

canceled;

theorem :: RFINSEQ:4

canceled;

theorem :: RFINSEQ:5

canceled;

theorem :: RFINSEQ:6

canceled;

theorem :: RFINSEQ:7

canceled;

theorem :: RFINSEQ:8

canceled;

theorem :: RFINSEQ:9

canceled;

theorem :: RFINSEQ:10

canceled;

theorem :: RFINSEQ:11

canceled;

theorem :: RFINSEQ:12

canceled;

theorem :: RFINSEQ:13

canceled;

registration

let f be FinSequence;
let x be set ;
cluster Coim (f,x) -> finite ;
coherence
Coim (f,x) is finite ;

end;

theorem Th14: :: RFINSEQ:14

for f, g, h being FinSequence holds
( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent )

proof end;

theorem :: RFINSEQ:15

for f, g being FinSequence holds f ^ g,g ^ f are_fiberwise_equipotent

proof end;

theorem Th16: :: RFINSEQ:16

for f, g being FinSequence st f,g are_fiberwise_equipotent holds
( len f = len g & dom f = dom g )

proof end;

theorem Th17: :: RFINSEQ:17

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

proof end;

defpred S₁[ 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: S₁[ 0 ]

proof end;

Lm2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof end;

theorem :: RFINSEQ:18

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

proof end;

definition

canceled;
let f be FinSequence;
let n be Nat;
func f /^ n -> FinSequence means :Def2: :: RFINSEQ:def 2
( 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 b₁ being FinSequence st
( len b₁ = (len f) - n & ( for m being Nat st m in dom b₁ holds
b₁ . m = f . (m + n) ) ) ) & ( not n <= len f implies ex b₁ being FinSequence st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence holds
( ( n <= len f & len b₁ = (len f) - n & ( for m being Nat st m in dom b₁ holds
b₁ . m = f . (m + n) ) & len b₂ = (len f) - n & ( for m being Nat st m in dom b₂ holds
b₂ . m = f . (m + n) ) implies b₁ = b₂ ) & ( not n <= len f & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being FinSequence holds verum ;

end;

:: deftheorem RFINSEQ:def 1 :
canceled;

:: deftheorem Def2 defines /^ RFINSEQ:def 2 :
for f being FinSequence
for n being Nat
for b₃ being FinSequence holds
( ( n <= len f implies ( b₃ = f /^ n iff ( len b₃ = (len f) - n & ( for m being Nat st m in dom b₃ holds
b₃ . m = f . (m + n) ) ) ) ) & ( not n <= len f implies ( b₃ = f /^ n iff b₃ = {} ) ) );

definition

let D be set ;
let f be FinSequence of D;
let n be Nat;
:: original: /^
redefine func f /^ n -> FinSequence of D;
coherence
f /^ n is FinSequence of D

proof end;

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 Th19: :: RFINSEQ:19

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 )

proof end;

theorem Th20: :: RFINSEQ:20

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

proof end;

theorem Th21: :: RFINSEQ:21

for D being non empty set
for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f

proof end;

theorem :: RFINSEQ:22

for R1, R2 being FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
Sum R1 = Sum R2

proof end;

definition

let R be FinSequence of REAL ;
func MIM R -> FinSequence of REAL means :Def3: :: RFINSEQ:def 3
( 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 b₁ being FinSequence of REAL st
( len b₁ = len R & b₁ . (len b₁) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b₁) - 1 holds
b₁ . n = (R . n) - (R . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len R & b₁ . (len b₁) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b₁) - 1 holds
b₁ . n = (R . n) - (R . (n + 1)) ) & len b₂ = len R & b₂ . (len b₂) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b₂) - 1 holds
b₂ . n = (R . n) - (R . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines MIM RFINSEQ:def 3 :
for R, b₂ being FinSequence of REAL holds
( b₂ = MIM R iff ( len b₂ = len R & b₂ . (len b₂) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b₂) - 1 holds
b₂ . n = (R . n) - (R . (n + 1)) ) ) );

theorem Th23: :: RFINSEQ:23

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

proof end;

theorem Th24: :: RFINSEQ:24

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

proof end;

theorem Th25: :: RFINSEQ:25

MIM (<*> REAL) = <*> REAL

proof end;

theorem Th26: :: RFINSEQ:26

for r being Real holds MIM <*r*> = <*r*>

proof end;

theorem :: RFINSEQ:27

for r, s being Real holds MIM <*r,s*> = <*(r - s),s*>

proof end;

theorem :: RFINSEQ:28

for R being FinSequence of REAL
for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n)

proof end;

theorem Th29: :: RFINSEQ:29

for R being FinSequence of REAL st len R <> 0 holds
Sum (MIM R) = R . 1

proof end;

theorem :: RFINSEQ:30

for R being FinSequence of REAL
for n being Element of NAT st n < len R holds
Sum (MIM (R /^ n)) = R . (n + 1)

proof end;

definition

let IT be FinSequence of REAL ;
redefine attr IT is non-increasing means :Def4: :: RFINSEQ:def 4
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) )

proof end;

end;

:: deftheorem Def4 defines non-increasing RFINSEQ:def 4 :
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 V47() V48() V49() non-increasing FinSequence of REAL ;
existence
ex b₁ being FinSequence of REAL st b₁ is non-increasing

proof end;

end;

theorem Th31: :: RFINSEQ:31

for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds
R is non-increasing

proof end;

theorem Th32: :: RFINSEQ:32

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 )

proof end;

theorem Th33: :: RFINSEQ:33

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

proof end;

theorem :: RFINSEQ:34

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

proof end;

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 )

proof end;

defpred S₂[ 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: S₂[ 0 ]

proof end;

Lm6: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof end;

theorem Th35: :: RFINSEQ:35

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 Element of 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:36

for R1, R2 being non-increasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
R1 = R2

proof end;

theorem :: RFINSEQ:37

for R being FinSequence of REAL
for r, s being Real st r <> 0 holds
R " {(s / r)} = (r * R) " {s}

proof end;

theorem :: RFINSEQ:38

for R being FinSequence of REAL holds (0 * R) " {0} = dom R

proof end;

begin

theorem :: RFINSEQ:39

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

proof end;

theorem :: RFINSEQ:40

for D being non empty set
for f being FinSequence of D holds f /^ (len f) = {}

proof end;

theorem :: RFINSEQ:41

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

proof end;

theorem :: RFINSEQ:42

for D being non empty set
for f being FinSequence of D
for k being Nat holds len (f /^ k) = (len f) -' k

proof end;

theorem Th43: :: RFINSEQ:43

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 )

proof end;

theorem Th44: :: RFINSEQ:44

for f, g, h being FinSequence holds
( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )

proof end;

theorem :: RFINSEQ:45

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 )

proof end;

theorem :: RFINSEQ:46

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 )

proof end;