:: Sorting Operators for Finite Sequences :: by Yatsuka Nakamura :: :: Received October 17, 2003 :: Copyright (c) 2003-2018 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, FINSEQ_1, CARD_1, XXREAL_0, RELAT_1, REAL_1, FUNCT_1, ARYTM_3, FUNCOP_1, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_2, XBOOLE_0, VALUED_0, ORDINAL4, NAT_1, RFINSEQ2; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, XCMPLX_0, XREAL_0, FUNCT_1, FUNCT_2, FINSEQ_1, REAL_1, NAT_1, RVSUM_1, FUNCOP_1, CLASSES1, RFINSEQ, INTEGRA2; constructors FUNCOP_1, REAL_1, NAT_1, BINOP_2, SEQM_3, RFINSEQ, INTEGRA2, RVSUM_1, CLASSES1, RELSET_1; registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, INTEGRA2, VALUED_0, FINSET_1, CARD_1, XREAL_0, ORDINAL1; 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 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; projectivity; 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 non-decreasing FinSequence of REAL means :: RFINSEQ2:def 6 ::Ascend Sorting or Rearrangement of FinSequences f,it are_fiberwise_equipotent; projectivity; 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; ::\$CT 2 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;