Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Sorting Operators for Finite Sequences

by
Yatsuka Nakamura

MML identifier: RFINSEQ2
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, CARD_1, FUNCT_1, BOOLE, FUNCT_2, FINSEQ_1, ARYTM_1,
SQUARE_1, PROB_1, RFINSEQ, RFINSEQ2, CQC_LANG;
notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
FINSEQ_1, CARD_1, REAL_1, NAT_1, SQUARE_1, SEQ_1, RVSUM_1, TOPREAL1,
CQC_LANG, RFINSEQ, INTEGRA2;
constructors REAL_1, NAT_1, SQUARE_1, TOPREAL1, SEQ_1, CQC_LANG, RFINSEQ,
INTEGRA2;
clusters NUMBERS, FUNCT_1, RELSET_1, FINSEQ_1, XREAL_0, FUNCT_2, REAL_1,
NAT_1, RFINSEQ, INTEGRA2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve n,m for Nat;

definition let f be FinSequence of REAL;
func max_p f -> Nat means
:: RFINSEQ2:def 1
(len f=0 implies it=0) &
(len f>0 implies
it in dom f &
(for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.it
holds r1<=r2) & (for j being Nat st j in dom f & f.j=f.it holds it<=j));
end;

definition let f be FinSequence of REAL;
func min_p f -> Nat means
:: RFINSEQ2:def 2
(len f=0 implies it=0) &
(len f>0 implies
it in dom f &
(for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.it
holds r1>=r2) & (for j being Nat st j in dom f & f.j=f.it holds it<=j));
end;

definition let f be FinSequence of REAL;
func max f -> Real equals
:: RFINSEQ2:def 3
f.(max_p f);
func min f -> Real equals
:: RFINSEQ2:def 4
f.(min_p f);
end;

theorem :: RFINSEQ2:1
for f being FinSequence of REAL,i being Nat
st 1<=i & i<=len f holds f.i<=f.(max_p f) & f.i<=max f;

theorem :: RFINSEQ2:2
for f being FinSequence of REAL,i being Nat
st 1<=i & i<=len f holds f.i>=f.(min_p f) & f.i>=min f;

theorem :: RFINSEQ2:3
for f being FinSequence of REAL,r being Real
st f=<*r*> holds max_p f=1 & max f=r;

theorem :: RFINSEQ2:4
for f being FinSequence of REAL,r being Real
st f=<*r*> holds min_p f=1 & min f=r;

theorem :: RFINSEQ2:5
for f being FinSequence of REAL,r1,r2 being Real
st f=<*r1,r2*> holds max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2);

theorem :: RFINSEQ2:6
for f being FinSequence of REAL,r1,r2 being Real
st f=<*r1,r2*> holds min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2);

theorem :: RFINSEQ2:7
for f1,f2 being FinSequence of REAL st len f1=len f2 & len f1>0
holds max (f1+f2)<=(max f1) +(max f2);

theorem :: RFINSEQ2:8
for f1,f2 being FinSequence of REAL st len f1=len f2 & len f1>0
holds min (f1+f2)>=(min f1) +(min f2);

theorem :: RFINSEQ2:9
for f being FinSequence of REAL, a being Real st len f>0 & a>0
holds max (a*f)=a*(max f) & max_p (a*f)=max_p f;

theorem :: RFINSEQ2:10
for f being FinSequence of REAL, a being Real st
len f>0 & a>0
holds min (a*f)=a*(min f) & min_p (a*f)=min_p f;

theorem :: RFINSEQ2:11
for f being FinSequence of REAL st
len f>0
holds max (-f)=-(min f) & max_p (-f)=min_p f;

theorem :: RFINSEQ2:12
for f being FinSequence of REAL st len f>0
holds min (-f)=-(max f) & min_p (-f)=max_p f;

theorem :: RFINSEQ2:13
for f being FinSequence of REAL,n being Nat st
1<=n & n<len f
holds max (f/^n)<= max f & min (f/^n)>= min f;

theorem :: RFINSEQ2:14
for f,g being FinSequence of REAL st
f,g are_fiberwise_equipotent holds max f=max g;

theorem :: RFINSEQ2:15
for f,g being FinSequence of REAL st
f,g are_fiberwise_equipotent holds min f=min g;

definition let f be FinSequence of REAL;
func sort_d f -> non-increasing FinSequence of REAL means
:: RFINSEQ2:def 5
::Descend Sorting or Rearrangement of FinSequences
f,it are_fiberwise_equipotent;
end;

theorem :: RFINSEQ2:16
for R be FinSequence of REAL
st len R = 0 or len R = 1 holds R is non-decreasing;

theorem :: RFINSEQ2:17
for R be FinSequence of REAL holds
R is non-decreasing
iff
for n,m be Nat st n in dom R & m in dom R & n<m holds R.n<=R.m;

theorem :: RFINSEQ2:18
for R be non-decreasing FinSequence of REAL, n be Nat holds
R|n is non-decreasing FinSequence of REAL;

theorem :: RFINSEQ2:19
for R1,R2 be non-decreasing FinSequence of REAL st
R1,R2 are_fiberwise_equipotent holds R1 = R2;

definition let f be FinSequence of REAL;
func sort_a f -> non-decreasing FinSequence of REAL means
:: RFINSEQ2:def 6
::Ascend Sorting or Rearrangement of FinSequences
f,it are_fiberwise_equipotent;
end;

theorem :: RFINSEQ2:20
for f being non-increasing FinSequence of REAL
holds sort_d f=f;

theorem :: RFINSEQ2:21
for f being non-decreasing FinSequence of REAL
holds sort_a f=f;

theorem :: RFINSEQ2:22
for f being FinSequence of REAL
holds sort_d (sort_d f)=sort_d f;

theorem :: RFINSEQ2:23
for f being FinSequence of REAL
holds sort_a (sort_a f)=sort_a f;

theorem :: RFINSEQ2:24
for f being FinSequence of REAL st f is non-increasing
holds -f is non-decreasing;

theorem :: RFINSEQ2:25
for f being FinSequence of REAL st f is non-decreasing
holds -f is non-increasing;

theorem :: RFINSEQ2:26
for f,g being FinSequence of REAL,P being Permutation of dom g
st f = g*P & len g>=1 holds -f=(-g)*P;

theorem :: RFINSEQ2:27
for f,g being FinSequence of REAL
st f,g are_fiberwise_equipotent holds -f,-g are_fiberwise_equipotent;

theorem :: RFINSEQ2:28
for f being FinSequence of REAL holds
sort_d (-f) = - (sort_a f);

theorem :: RFINSEQ2:29
for f being FinSequence of REAL holds
sort_a (-f) = - (sort_d f);

theorem :: RFINSEQ2:30
for f being FinSequence of REAL holds
dom (sort_d f)=dom f & len (sort_d f)=len f;

theorem :: RFINSEQ2:31
for f being FinSequence of REAL holds
dom (sort_a f)=dom f & len (sort_a f)=len f;

theorem :: RFINSEQ2:32
for f being FinSequence of REAL st
len f >=1 holds
max_p(sort_d f)=1 & min_p(sort_a f)=1
& (sort_d f).1=max f & (sort_a f).1=min f;

```