begin
:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :
for f being FinSequence of REAL
for b2 being Element of NAT holds
( b2 = max_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );
:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :
for f being FinSequence of REAL
for b2 being Element of NAT holds
( b2 = min_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );
:: deftheorem defines max RFINSEQ2:def 3 :
for f being FinSequence of REAL holds max f = f . (max_p f);
:: deftheorem defines min RFINSEQ2:def 4 :
for f being FinSequence of REAL holds min f = f . (min_p f);
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f <= max g
theorem Th14:
Lm2:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f >= min g
theorem Th15:
:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
for f being FinSequence of REAL
for b2 being non-increasing FinSequence of REAL holds
( b2 = sort_d f iff f,b2 are_fiberwise_equipotent );
theorem Th16:
theorem Th17:
Lm3:
for f, g being non-decreasing 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 )
theorem Th18:
Lm4:
for n being Element of NAT
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
theorem Th19:
:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
for f being FinSequence of REAL
for b2 being non-decreasing FinSequence of REAL holds
( b2 = sort_a f iff f,b2 are_fiberwise_equipotent );
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem Th30:
theorem Th31:
theorem