:: 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; definitions INTEGRA2; equalities RELAT_1; expansions INTEGRA2; theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, NAT_1, FUNCT_1, FUNCT_2, RVSUM_1, RELAT_1, FUNCOP_1, RFINSEQ, INTEGRA2, XREAL_1, XXREAL_0, VALUED_1, CLASSES1; schemes NAT_1; begin reserve n,m for Nat; definition let f be FinSequence of REAL; func max_p f -> Nat means :Def1: (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 ); existence proof A1: dom f=Seg len f by FINSEQ_1:def 3; per cases; suppose len f=0; hence thesis; end; suppose A2: len f<>0; defpred P[Nat] means (ex n being Nat st (\$1<>0 implies n<=\$1 & n in dom f) & (for i being Nat, r1,r2 being Real st i <=\$1 & i in dom f & r1=f.i & r2=f.n holds r1<=r2) & (for j being Nat st j<=\$1 & j in dom f & f.j=f.n holds n<=j)); A3: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then consider n1 being Nat such that A4: k<>0 implies n1<=k & n1 in dom f and A5: for i being Nat,r1,r2 being Real st i<=k & i in dom f & r1=f.i & r2=f.n1 holds r1<=r2 and A6: for j being Nat st j<=k & j in dom f & f.j=f.n1 holds n1<=j; per cases; suppose A7: k=0; A8: dom f=Seg len f by FINSEQ_1:def 3; A9: for i being Nat,r1,r2 being Real st i<=1 & i in dom f & r1=f.i & r2=f.1 holds r1<=r2 proof let i be Nat,r1,r2 be Real; assume that A10: i<=1 and A11: i in dom f and A12: r1=f.i & r2=f.1; 1<=i by A11,FINSEQ_3:25; hence thesis by A10,A12,XXREAL_0:1; end; len f>=0+1 by A2,NAT_1:13; then A13: 1 in dom f by A8,FINSEQ_1:1; for j being Nat st j<=1 & j in dom f & f.j=f.1 holds 1<=j by A8,FINSEQ_1:1; hence thesis by A7,A13,A9; end; suppose A14: k<>0; now per cases; case A15: f.n1>=f.(k+1); A16: for i being Nat, r1,r2 being Real st i<=k+1 & i in dom f & r1=f.i & r2=f.n1 holds r1<=r2 proof let i be Nat,r1,r2 be Real; assume that A17: i<=k+1 and A18: i in dom f and A19: r1=f.i & r2=f.n1; per cases; suppose i=k+1; hence thesis by A15,A17,A19,XXREAL_0:1; end; end; A20: n1<=k+1 by A4,A14,NAT_1:13; A21: for j being Nat st j<=k+1 & j in dom f & f.j=f. n1 holds n1<=j proof let j be Nat; assume that A22: j<=k+1 and A23: j in dom f & f.j=f.n1; now per cases; case j=k+1; hence thesis by A20,A22,XXREAL_0:1; end; end; hence thesis; end; k+1<>0 implies n1<=k+1 & n1 in dom f by A4,A14,NAT_1:13; hence thesis by A16,A21; end; case A24: f.n1len f; A26: for j being Nat st j<=k+1 & j in dom f & f.j =f.n1 holds n1<=j proof let j be Nat; assume that j<=k+1 and A27: j in dom f & f.j=f.n1; per cases; suppose j=k+1; then k=len f by A25,NAT_1:13; A29: for i being Nat, r1,r2 being Real st i<=k+1 & i in dom f & r1=f.i & r2=f.n1 holds r1<=r2 proof let i be Nat,r1,r2 be Real; assume that i<=k+1 and A30: i in dom f and A31: r1=f.i & r2=f.n1; i<=len f by A1,A30,FINSEQ_1:1; then i<=k by A28,XXREAL_0:2; hence thesis by A5,A30,A31; end; n1<=len f by A1,A4,A14,FINSEQ_1:1; then k+1<>0 implies n1<=k+1 & n1 in dom f by A4,A14,A25,XXREAL_0:2; hence thesis by A29,A26; end; case A32: k+1<=len f; set n2=k+1; A33: for i being Nat, r1,r2 being Real st i<=k+1 & i in dom f & r1=f.i & r2=f.n2 holds r1<=r2 proof let i be Nat,r1,r2 be Real; assume that A34: i<=k+1 and A35: i in dom f and A36: r1=f.i and A37: r2=f.n2; per cases; suppose A38: i=k+1; hence thesis by A34,A36,A37,XXREAL_0:1; end; end; A39: for j being Nat st j<=k+1 & j in dom f & f.j =f.n2 holds n2<=j proof let j be Nat; assume that j<=k+1 and A40: j in dom f & f.j=f.n2; per cases; suppose j=k+1; hence thesis; end; end; 1<=1+k by NAT_1:12; then k+1<>0 implies n2<=k+1 & n2 in dom f by A1,A32, FINSEQ_1:1; hence thesis by A33,A39; end; end; hence thesis; end; end; hence thesis; end; end; ( for i being Nat, r1,r2 being Real st i<=0 & i in dom f & r1=f.i & r2=f.1 holds r1<=r2)& for j being Nat st j<=0 & j in dom f & f.j=f. 1 holds 1<=j by A1,FINSEQ_1:1; then A41: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A41,A3); then consider n1 being Nat such that A42: len f<>0 implies n1<=len f & n1 in dom f and A43: for i being Nat,r1,r2 being Real st i<=len f & i in dom f & r1=f.i & r2=f.n1 holds r1<=r2 and A44: for j being Nat st j<=len f & j in dom f & f.j=f.n1 holds n1<=j; A45: for j being Nat st j in dom f & f.j=f.n1 holds n1<=j proof let j be Nat; assume that A46: j in dom f and A47: f.j=f.n1; j<=len f by A46,FINSEQ_3:25; hence thesis by A44,A46,A47; end; for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.n1 holds r1<=r2 proof let i be Nat,r1,r2 be Real; assume that A48: i in dom f and A49: r1=f.i & r2=f.n1; i<=len f by A48,FINSEQ_3:25; hence thesis by A43,A48,A49; end; hence thesis by A2,A42,A45; end; end; uniqueness proof thus for m1,m2 being Nat st (len f=0 implies m1=0) & (len f>0 implies m1 in dom f & (for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.m1 holds r1<=r2) & for j being Nat st j in dom f & f.j=f.m1 holds m1<=j ) & (len f=0 implies m2=0) & (len f>0 implies m2 in dom f & (for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.m2 holds r1<=r2) & for j being Nat st j in dom f & f.j=f.m2 holds m2<=j ) holds m1=m2 proof let m1,m2 be Nat; assume A50: ( len f=0 implies m1=0)&( len f>0 implies m1 in dom f & (for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.m1 holds r1 <=r2) & for j being Nat st j in dom f & f.j=f.m1 holds m1<=j) & ( len f=0 implies m2=0)&( len f>0 implies m2 in dom f & (for i being Nat, r1,r2 being Real st i in dom f & r1=f.i & r2=f.m2 holds r1<=r2) & for j being Nat st j in dom f & f.j=f.m2 holds m2<=j); then f.m2<=f.m1 & f.m1<=f.m2; then f.m1=f.m2 by XXREAL_0:1; then m1<=m2 & m2<=m1 by A50; hence thesis by XXREAL_0:1; end; end; end; definition let f be FinSequence of REAL; func min_p f -> Nat means :Def2: (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 ); existence proof A1: dom f=Seg len f by FINSEQ_1:def 3; now per cases; case len f=0; hence thesis; end; case A2: len f<>0; defpred P[Nat] means (ex n being Nat st (\$1<>0 implies n<=\$1 & n in dom f) & (for i being Nat, r1,r2 being Real st i <=\$1 & i in dom f & r1=f.i & r2=f.n holds r1>=r2) & (for j being Nat st j<=\$1 & j in dom f & f.j=f.n holds n<=j)); A3: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then consider n1 being Nat such that A4: k<>0 implies n1<=k & n1 in dom f and A5: for i being Nat,r1,r2 being Real st i<=k & i in dom f & r1=f.i & r2=f.n1 holds r1>=r2 and A6: for j being Nat st j<=k & j in dom f & f.j=f.n1 holds n1<=j; now per cases; case A7: k=0; A8: dom f=Seg len f by FINSEQ_1:def 3; A9: for i being Nat, r1,r2 being Real st i<=1 & i in dom f & r1=f.i & r2=f.1 holds r1>=r2 proof let i be Nat,r1,r2 be Real; assume that A10: i<=1 and A11: i in dom f and A12: r1=f.i & r2=f.1; 1<=i by A11,FINSEQ_3:25; hence thesis by A10,A12,XXREAL_0:1; end; len f>=0+1 by A2,NAT_1:13; then A13: 1 in dom f by A8,FINSEQ_1:1; for j being Nat st j<=1 & j in dom f & f.j=f.1 holds 1<=j by A8,FINSEQ_1:1; hence thesis by A7,A13,A9; end; case A14: k<>0; now per cases; case A15: f.n1<=f.(k+1); A16: for i being Nat, r1,r2 being Real st i<=k+1 & i in dom f & r1=f.i & r2=f.n1 holds r1>=r2 proof let i be Nat,r1,r2 be Real; assume that A17: i<=k+1 and A18: i in dom f and A19: r1=f.i & r2=f.n1; per cases; suppose i=k+1; hence thesis by A15,A17,A19,XXREAL_0:1; end; end; A20: n1<=k+1 by A4,A14,NAT_1:13; A21: for j being Nat st j<=k+1 & j in dom f & f.j =f.n1 holds n1<=j proof let j be Nat; assume that A22: j<=k+1 and A23: j in dom f & f.j=f.n1; per cases; suppose j=k+1; hence thesis by A20,A22,XXREAL_0:1; end; end; k+1<>0 implies n1<=k+1 & n1 in dom f by A4,A14,NAT_1:13; hence thesis by A16,A21; end; case A24: f.n1>f.(k+1); now per cases; case A25: k+1>len f; A26: for j being Nat st j<=k+1 & j in dom f & f.j=f.n1 holds n1<=j proof let j be Nat; assume that j<=k+1 and A27: j in dom f & f.j=f.n1; per cases; suppose j=k+1; then k=len f by A25,NAT_1:13; A29: for i being Nat, r1,r2 being Real st i<=k +1 & i in dom f & r1=f.i & r2=f.n1 holds r1>=r2 proof let i be Nat,r1,r2 be Real; assume that i<=k+1 and A30: i in dom f and A31: r1=f.i & r2=f.n1; i<=len f by A1,A30,FINSEQ_1:1; then i<=k by A28,XXREAL_0:2; hence thesis by A5,A30,A31; end; n1<=len f by A1,A4,A14,FINSEQ_1:1; then k +1<>0 implies n1<=k+1 & n1 in dom f by A4,A14,A25, XXREAL_0:2; hence thesis by A29,A26; end; case A32: k+1<=len f; set n2=k+1; A33: for i being Nat, r1,r2 being Real st i<=k +1 & i in dom f & r1=f.i & r2=f.n2 holds r1>=r2 proof let i be Nat,r1,r2 be Real; assume that A34: i<=k+1 and A35: i in dom f and A36: r1=f.i and A37: r2=f.n2; per cases; suppose A38: i=r3 by A5,A35,A36; hence thesis by A24,A37,XXREAL_0:2; end; suppose i>=k+1; hence thesis by A34,A36,A37,XXREAL_0:1; end; end; A39: for j being Nat st j<=k+1 & j in dom f & f.j=f.n2 holds n2<=j proof let j be Nat; assume that j<=k+1 and A40: j in dom f & f.j=f.n2; per cases; suppose j=k+1; hence thesis; end; end; 1<=1+k by NAT_1:12; then k+1<>0 implies n2<=k+1 & n2 in dom f by A1,A32, FINSEQ_1:1; hence thesis by A33,A39; end; end; hence thesis; end; end; hence thesis; end; end; hence thesis; end; ( for i being Nat, r1,r2 being Real st i<=0 & i in dom f & r1=f.i & r2=f.1 holds r1>=r2)& for j being Nat st j<=0 & j in dom f & f.j=f. 1 holds 1<=j by A1,FINSEQ_1:1; then A41: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A41,A3 ); then consider n1 being Nat such that A42: len f<>0 implies n1<=len f & n1 in dom f and A43: for i being Nat, r1,r2 being Real st i<=len f & i in dom f & r1=f.i & r2=f.n1 holds r1>=r2 and A44: for j being Nat st j<=len f & j in dom f & f.j=f. n1 holds n1<=j; A45: for j being Nat st j in dom f & f.j=f.n1 holds n1<=j proof let j be Nat; assume that A46: j in dom f and A47: f.j=f.n1; j<=len f by A46,FINSEQ_3:25; hence thesis by A44,A46,A47; end; for i being Nat, r1,r2 being Real st i in dom f & r1=f. i & r2=f.n1 holds r1>=r2 proof let i be Nat,r1,r2 be Real; assume that A48: i in dom f and A49: r1=f.i & r2=f.n1; i<=len f by A48,FINSEQ_3:25; hence thesis by A43,A48,A49; end; hence thesis by A2,A42,A45; end; end; hence thesis; end; uniqueness proof thus for m1,m2 being Nat st (len f=0 implies m1=0) & (len f>0 implies m1 in dom f & (for i being Nat, r1,r2 being Real st i in dom f & r1=f.i & r2=f.m1 holds r1>=r2) & for j being Nat st j in dom f & f.j=f.m1 holds m1<=j ) & (len f=0 implies m2=0) & (len f>0 implies m2 in dom f & (for i being Nat, r1,r2 being Real st i in dom f & r1=f.i & r2=f.m2 holds r1>=r2) & for j being Nat st j in dom f & f.j=f.m2 holds m2<=j ) holds m1=m2 proof let m1,m2 be Nat; assume A50: ( len f=0 implies m1=0)&( len f>0 implies m1 in dom f & (for i being Nat, r1,r2 being Real st i in dom f & r1=f.i & r2=f.m1 holds r1 >=r2) & for j being Nat st j in dom f & f.j=f.m1 holds m1<=j) & ( len f=0 implies m2=0)&( len f>0 implies m2 in dom f & (for i being Nat, r1,r2 being Real st i in dom f & r1=f.i & r2=f.m2 holds r1>=r2) & for j being Nat st j in dom f & f.j=f.m2 holds m2<=j); then f.m2>=f.m1 & f.m1>=f.m2; then f.m1=f.m2 by XXREAL_0:1; then m1>=m2 & m2>=m1 by A50; hence thesis by XXREAL_0:1; end; end; end; definition let f be FinSequence of REAL; func max f -> Real equals f.(max_p f); correctness; func min f -> Real equals f.(min_p f); correctness; end; theorem Th1: 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 proof let f be FinSequence of REAL,i be Nat; assume A1: 1<=i & i<=len f; then A2: i in dom f by FINSEQ_3:25; hence f.i<=f.(max_p f) by A1,Def1; thus thesis by A1,A2,Def1; end; theorem Th2: 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 proof let f be FinSequence of REAL,i be Nat; assume A1: 1<=i & i<=len f; then A2: i in dom f by FINSEQ_3:25; hence f.i>=f.(min_p f) by A1,Def2; thus thesis by A1,A2,Def2; end; theorem for f being FinSequence of REAL,r being Real st f=<*r*> holds max_p f= 1 & max f=r proof let f be FinSequence of REAL,r be Real; assume A1: f=<*r*>; then A2: f.1=r by FINSEQ_1:40; A3: len f=1 by A1,FINSEQ_1:40; then (max_p f) in dom f by Def1; then 1<= (max_p f) & (max_p f)<=len f by FINSEQ_3:25; hence thesis by A3,A2,XXREAL_0:1; end; theorem for f being FinSequence of REAL,r being Real st f=<*r*> holds min_p f= 1 & min f=r proof let f be FinSequence of REAL,r be Real; assume A1: f=<*r*>; then A2: f.1=r by FINSEQ_1:40; A3: len f=1 by A1,FINSEQ_1:40; then (min_p f) in dom f by Def2; then 1<= (min_p f) & (min_p f)<=len f by FINSEQ_3:25; hence thesis by A3,A2,XXREAL_0:1; end; theorem 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) proof let f be FinSequence of REAL,r1,r2 be Real; assume A1: f=<*r1,r2*>; then A2: len f=2 by FINSEQ_1:44; then A3: f.2<=f.(max_p f) by Th1; A4: f.1=r1 by A1,FINSEQ_1:44; A5: (max_p f) in dom f by A2,Def1; then A6: 1<= (max_p f) by FINSEQ_3:25; A7: (max_p f)<=len f by A5,FINSEQ_3:25; A8: f.2=r2 by A1,FINSEQ_1:44; A9: f.1<=f.(max_p f) by A2,Th1; now per cases; case r1>=r2; then A10: max(r1,r2)<=max f by A4,A9,XXREAL_0:def 10; now per cases; case max_p f=len f; then A12: max_p f=2 by A2,A7,XXREAL_0:1; then max f <=max(r1,r2) by A8,XXREAL_0:25; then A13: max f=max(r1,r2) by A10,XXREAL_0:1; 1 in dom f by A2,FINSEQ_3:25; then r1<>r2 by A2,A4,A8,A12,Def1; hence thesis by A8,A12,A13,FUNCOP_1:def 8; end; end; hence thesis; end; case r1=len f; then A16: max_p f=2 by A2,A7,XXREAL_0:1; then max f <=max(r1,r2) by A8,XXREAL_0:25; then A17: max f=max(r1,r2) by A14,XXREAL_0:1; 1 in dom f by A2,FINSEQ_3:25; then r1<>r2 by A2,A4,A8,A16,Def1; hence thesis by A8,A16,A17,FUNCOP_1:def 8; end; end; hence thesis; end; end; hence thesis; end; theorem 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) proof let f be FinSequence of REAL,r1,r2 be Real; assume A1: f=<*r1,r2*>; then A2: len f=2 by FINSEQ_1:44; then A3: f.1>=f.(min_p f) by Th2; A4: f.2=r2 by A1,FINSEQ_1:44; A5: (min_p f) in dom f by A2,Def2; then A6: 1<= (min_p f) by FINSEQ_3:25; A7: f.2>=f.(min_p f) by A2,Th2; A8: f.1=r1 by A1,FINSEQ_1:44; A9: (min_p f)<=len f by A5,FINSEQ_3:25; per cases; suppose r1<=r2; then A10: min(r1,r2)>=min f by A8,A3,XXREAL_0:def 9; now per cases; case min_p f=min(r1,r2) by A8,XXREAL_0:17; then min f=min(r1,r2) by A10,XXREAL_0:1; hence thesis by A8,A11,FUNCOP_1:def 8; end; case min_p f>=len f; then A12: min_p f=2 by A2,A9,XXREAL_0:1; then min f >=min(r1,r2) by A4,XXREAL_0:17; then A13: min f=min(r1,r2) by A10,XXREAL_0:1; 1 in dom f by A2,FINSEQ_3:25; then r1<>r2 by A2,A8,A4,A12,Def2; hence thesis by A4,A12,A13,FUNCOP_1:def 8; end; end; hence thesis; end; suppose r1>r2; then A14: min(r1,r2)>=min f by A4,A7,XXREAL_0:def 9; now per cases; case min_p f=min(r1,r2) by A8,XXREAL_0:17; then min f=min(r1,r2) by A14,XXREAL_0:1; hence thesis by A8,A15,FUNCOP_1:def 8; end; case min_p f>=len f; then A16: min_p f=2 by A2,A9,XXREAL_0:1; then min f >=min(r1,r2) by A4,XXREAL_0:17; then A17: min f=min(r1,r2) by A14,XXREAL_0:1; 1 in dom f by A2,FINSEQ_3:25; then r1<>r2 by A2,A8,A4,A16,Def2; hence thesis by A4,A16,A17,FUNCOP_1:def 8; end; end; hence thesis; end; end; theorem for f1,f2 being FinSequence of REAL st len f1=len f2 & len f1>0 holds max (f1+f2)<=(max f1) +(max f2) proof let f1,f2 be FinSequence of REAL; assume that A1: len f1=len f2 and A2: len f1>0; A3: len (f1+f2)=len f1 by A1,RVSUM_1:115; then A4: max_p (f1+f2) in dom (f1+f2) by A2,Def1; then 1<=max_p (f1+f2) & max_p (f1+f2)<=len (f1+f2) by FINSEQ_3:25; then A5: max_p (f1+f2) in Seg len f1 by A3,FINSEQ_1:1; then max_p (f1+f2) in dom f2 by A1,FINSEQ_1:def 3; then A6: f2.(max_p (f1+f2))<=f2.(max_p f2) by A1,A2,Def1; max_p (f1+f2) in dom f1 by A5,FINSEQ_1:def 3; then A7: f1.(max_p (f1+f2))<=f1.(max_p f1) by A2,Def1; max (f1+f2)=f1.(max_p (f1+f2)) + f2.(max_p (f1+f2)) by A4,VALUED_1:def 1; hence thesis by A7,A6,XREAL_1:7; end; theorem for f1,f2 being FinSequence of REAL st len f1=len f2 & len f1>0 holds min (f1+f2)>=(min f1) +(min f2) proof let f1,f2 be FinSequence of REAL; assume that A1: len f1=len f2 and A2: len f1>0; A3: len (f1+f2)=len f1 by A1,RVSUM_1:115; then A4: min_p (f1+f2) in dom (f1+f2) by A2,Def2; then 1<=min_p (f1+f2) & min_p (f1+f2)<=len (f1+f2) by FINSEQ_3:25; then A5: min_p (f1+f2) in Seg len f1 by A3,FINSEQ_1:1; then min_p (f1+f2) in dom f2 by A1,FINSEQ_1:def 3; then A6: f2.(min_p (f1+f2))>=f2.(min_p f2) by A1,A2,Def2; min_p (f1+f2) in dom f1 by A5,FINSEQ_1:def 3; then A7: f1.(min_p (f1+f2))>=f1.(min_p f1) by A2,Def2; min (f1+f2)=f1.(min_p (f1+f2)) + f2.(min_p (f1+f2)) by A4,VALUED_1:def 1; hence thesis by A7,A6,XREAL_1:7; end; theorem 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 proof let f be FinSequence of REAL, a be Real; assume that A1: len f>0 and A2: a>0; A3: len (a*f)=len f by RVSUM_1:117; then A4: max_p (a*f) in dom (a*f) by A1,Def1; then 1<=max_p (a*f) & max_p (a*f)<=len (a*f) by FINSEQ_3:25; then max_p (a*f) in Seg len f by A3,FINSEQ_1:1; then A5: max_p (a*f) in dom f by FINSEQ_1:def 3; then f.(max_p (f))>= f.(max_p (a*f)) by A1,Def1; then A6: a*(f.(max_p (f)))>=a*(f.(max_p (a*f))) by A2,XREAL_1:64; A7: a*(f.(max_p (f)))=(a*f).(max_p (f)) & a*(f.(max_p (a*f)))=(a*f).(max_p (a*f) ) by RVSUM_1:44; A8: dom (a*f)=dom f by VALUED_1:def 5; then A9: max_p (f) in dom (a*f) by A1,Def1; then (a*f).(max_p (f))<=(a*f).(max_p (a*f)) by A1,A3,Def1; then A10: f.(max_p (f))<=f.(max_p (a*f)) by A2,A7,XREAL_1:68; f.(max_p (a*f))<=f.(max_p f) by A1,A5,Def1; then f.(max_p (f))=f.(max_p (a*f)) by A10,XXREAL_0:1; then A11: max (a*f)=a*(f.(max_p (a*f))) & max_p (a*f)>=max_p f by A1,A8,A4,Def1, RVSUM_1:44; max_p (f) in dom (a*f) by A1,A8,Def1; then (a*f).(max_p (a*f))>=(a*f).(max_p f) by A1,A3,Def1; then (a*f).(max_p (a*f))=(a*f).(max_p f) by A7,A6,XXREAL_0:1; then max_p (a*f)<=max_p f by A1,A3,A9,Def1; hence thesis by A11,XXREAL_0:1; end; theorem 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 proof let f be FinSequence of REAL, a be Real; assume that A1: len f>0 and A2: a>0; A3: len (a*f)=len f by RVSUM_1:117; then A4: min_p (a*f) in dom (a*f) by A1,Def2; then 1<=min_p (a*f) & min_p (a*f)<=len (a*f) by FINSEQ_3:25; then A5: min_p (a*f) in dom f by A3,FINSEQ_3:25; then f.(min_p (f))<= f.(min_p (a*f)) by A1,Def2; then A6: a*(f.(min_p (f)))<=a*(f.(min_p (a*f))) by A2,XREAL_1:64; A7: a*(f.(min_p (f)))=(a*f).(min_p (f)) & a*(f.(min_p (a*f)))=(a*f).(min_p ( a*f) ) by RVSUM_1:44; A8: dom (a*f)=dom f by VALUED_1:def 5; then A9: min_p (f) in dom (a*f) by A1,Def2; then (a*f).(min_p (f))>=(a*f).(min_p (a*f)) by A1,A3,Def2; then A10: f.(min_p (f))>=f.(min_p (a*f)) by A2,A7,XREAL_1:68; f.(min_p (a*f))>=f.(min_p f) by A1,A5,Def2; then f.(min_p (f))=f.(min_p (a*f)) by A10,XXREAL_0:1; then A11: min (a*f)=a*(f.(min_p (a*f))) & min_p (a*f)>=min_p f by A1,A8,A4,Def2, RVSUM_1:44; min_p (f) in dom (a*f) by A1,A8,Def2; then (a*f).(min_p (a*f))<=(a*f).(min_p f) by A1,A3,Def2; then (a*f).(min_p (a*f))=(a*f).(min_p f) by A7,A6,XXREAL_0:1; then min_p (a*f)<=min_p f by A1,A3,A9,Def2; hence thesis by A11,XXREAL_0:1; end; theorem for f being FinSequence of REAL st len f>0 holds max (-f)=-(min f) & max_p (-f)=min_p f proof let f be FinSequence of REAL; assume A1: len f>0; A2: len (-f)=len f by RVSUM_1:114; then A3: max_p (-f) in dom (-f) by A1,Def1; then 1<=max_p (-f) & max_p (-f)<=len (-f) by FINSEQ_3:25; then max_p (-f) in Seg len f by A2,FINSEQ_1:1; then A4: max_p (-f) in dom f by FINSEQ_1:def 3; then f.(min_p (f))<= f.(max_p (-f)) by A1,Def2; then A5: -(f.(min_p (f)))>=-(f.(max_p (-f))) by XREAL_1:24; A6: -(f.(min_p (f)))=(-f).(min_p (f)) & -(f.(max_p (-f)))=(-f).(max_p (-f)) by RVSUM_1:17; A7: dom (-f)=dom f by VALUED_1:8; then A8: min_p (f) in dom (-f) by A1,Def2; then (-f).(max_p (-f))>=(-f).(min_p f) by A1,A2,Def1; then A9: f.(max_p (-f))<=f.(min_p f) by A6,XREAL_1:24; f.(min_p (f))<=f.(max_p (-f)) by A1,A4,Def2; then f.(min_p (f))=f.(max_p (-f)) by A9,XXREAL_0:1; then A10: max (-f)=-(f.(max_p (-f))) & max_p (-f)>=min_p f by A1,A7,A3,Def2, RVSUM_1:17; min_p (f) in dom (-f) by A1,A7,Def2; then (-f).(max_p (-f))>=(-f).(min_p f) by A1,A2,Def1; then (-f).(max_p (-f))=(-f).(min_p f) by A6,A5,XXREAL_0:1; then max_p (-f)<=min_p f by A1,A2,A8,Def1; hence thesis by A10,XXREAL_0:1; end; theorem for f being FinSequence of REAL st len f>0 holds min (-f)=-(max f) & min_p (-f)=max_p f proof let f be FinSequence of REAL; assume A1: len f>0; A2: len (-f)=len f by RVSUM_1:114; then A3: min_p (-f) in dom (-f) by A1,Def2; then 1<=min_p (-f) & min_p (-f)<=len (-f) by FINSEQ_3:25; then min_p (-f) in Seg len f by A2,FINSEQ_1:1; then A4: min_p (-f) in dom f by FINSEQ_1:def 3; then f.(max_p (f))>= f.(min_p (-f)) by A1,Def1; then A5: -(f.(max_p (f)))<=-(f.(min_p (-f))) by XREAL_1:24; A6: -(f.(max_p (f)))=(-f).(max_p (f)) & -(f.(min_p (-f)))=(-f).(min_p (-f)) by RVSUM_1:17; A7: dom (-f)=dom f by VALUED_1:8; then A8: max_p (f) in dom (-f) by A1,Def1; then (-f).(min_p (-f))<=(-f).(max_p f) by A1,A2,Def2; then A9: f.(min_p (-f))>=f.(max_p f) by A6,XREAL_1:24; f.(max_p (f))>=f.(min_p (-f)) by A1,A4,Def1; then f.(max_p (f))=f.(min_p (-f)) by A9,XXREAL_0:1; then A10: min (-f)=-(f.(min_p (-f))) & min_p (-f)>=max_p f by A1,A7,A3,Def1, RVSUM_1:17; max_p (f) in dom (-f) by A1,A7,Def1; then (-f).(min_p (-f))<=(-f).(max_p f) by A1,A2,Def2; then (-f).(min_p (-f))=(-f).(max_p f) by A6,A5,XXREAL_0:1; then min_p (-f)<=max_p f by A1,A2,A8,Def2; hence thesis by A10,XXREAL_0:1; end; theorem for f being FinSequence of REAL,n being Nat st n= min f proof let f be FinSequence of REAL,n be Nat; A1: 1<=1+n by NAT_1:12; assume A2: n0 by A2,XREAL_1:50; then A5: (min_p (f/^n)) in dom (f/^n) by Def2; then A6: f.( (min_p (f/^n))+n)=min (f/^n) by A2,RFINSEQ:def 1; (min_p (f/^n))<=len (f/^n) by A5,FINSEQ_3:25; then A7: (min_p (f/^n))+n<=len f-n+n by A3,XREAL_1:7; A8: 1<=1+n by NAT_1:12; 1<= (min_p (f/^n)) by A5,FINSEQ_3:25; then 1+n<=(min_p (f/^n))+n by XREAL_1:7; then 1<= ((min_p (f/^n))+n) by A8,XXREAL_0:2; then A9: ((min_p (f/^n))+n) in dom f by A7,FINSEQ_3:25; A10: (max_p (f/^n)) in dom (f/^n) by A4,Def1; then (max_p (f/^n))<=len (f/^n) by FINSEQ_3:25; then A11: (max_p (f/^n))+n<=len f-n+n by A3,XREAL_1:7; 1<= (max_p (f/^n)) by A10,FINSEQ_3:25; then 1+n<=(max_p (f/^n))+n by XREAL_1:7; then 1<= ((max_p (f/^n))+n) by A1,XXREAL_0:2; then A12: ((max_p (f/^n))+n) in dom f by A11,FINSEQ_3:25; f.( (max_p (f/^n))+n)=max (f/^n) by A2,A10,RFINSEQ:def 1; hence thesis by A2,A12,A9,A6,Def1,Def2; end; Lm1: for f,g being FinSequence of REAL st f,g are_fiberwise_equipotent holds max f<=max g proof let f,g be FinSequence of REAL; assume A1: f,g are_fiberwise_equipotent; then consider P being Permutation of dom g such that A2: f = g*P by RFINSEQ:4; A3: dom f=dom g by A1,RFINSEQ:3; A4: len f=len g by A1,RFINSEQ:3; per cases; suppose A5: len f>0; then A6: max_p f in dom (g*P) by A2,Def1; then A7: (g*P).(max_p f)=g.(P.(max_p f)) by FUNCT_1:12; dom g=Seg len g by FINSEQ_1:def 3; then dom P=dom g by A4,A5,FUNCT_2:def 1; then A8: rng P=dom g & P.(max_p f) in rng P by A2,A3,A6,FUNCT_1:def 3,FUNCT_2:def 3; reconsider n=P.(max_p f) as Nat; dom g=Seg len g by FINSEQ_1:def 3; then 1<=n & n<=len g by A8,FINSEQ_1:1; hence thesis by A2,A7,Th1; end; suppose len f<=0; then f={} & g = {} by A4; hence thesis; end; end; theorem Th14: for f,g being FinSequence of REAL st f,g are_fiberwise_equipotent holds max f=max g proof let f,g be FinSequence of REAL; assume f,g are_fiberwise_equipotent; then max f <= max g & max g <= max f by Lm1; hence thesis by XXREAL_0:1; end; Lm2: for f,g being FinSequence of REAL st f,g are_fiberwise_equipotent holds min f>=min g proof let f,g be FinSequence of REAL; assume A1: f,g are_fiberwise_equipotent; then consider P being Permutation of dom g such that A2: f = g*P by RFINSEQ:4; A3: len f=len g by A1,RFINSEQ:3; per cases; suppose A4: len f>0; dom g=Seg len g by FINSEQ_1:def 3; then A5: dom P=dom g by A3,A4,FUNCT_2:def 1; A6: min_p f in dom (g*P) by A2,A4,Def2; then A7: (g*P).(min_p f)=g.(P.(min_p f)) by FUNCT_1:12; min_p f in dom g by A1,A2,A6,RFINSEQ:3; then A8: rng P=dom g & P.(min_p f) in rng P by A5,FUNCT_1:def 3,FUNCT_2:def 3; reconsider n=P.(min_p f) as Nat; dom g=Seg len g by FINSEQ_1:def 3; then 1<=n & n<=len g by A8,FINSEQ_1:1; hence thesis by A2,A7,Th2; end; suppose len f<=0; then f={} & g = {} by A3; hence thesis; end; end; theorem Th15: for f,g being FinSequence of REAL st f,g are_fiberwise_equipotent holds min f=min g proof let f,g be FinSequence of REAL; assume f,g are_fiberwise_equipotent; then min f >= min g & min g >= min f by Lm2; hence thesis by XXREAL_0:1; end; definition let f be FinSequence of REAL; func sort_d f -> non-increasing FinSequence of REAL means ::Descend Sorting or Rearrangement of FinSequences :Def5: f,it are_fiberwise_equipotent; existence by RFINSEQ:22; uniqueness by CLASSES1:76,RFINSEQ:23; projectivity; end; theorem Th16: for R be FinSequence of REAL st len R = 0 or len R = 1 holds R is non-decreasing proof let R be FinSequence of REAL; assume A1: len R = 0 or len R = 1; per cases by A1; suppose len R = 0; then R = <*>REAL; then for n st n in dom R & n+1 in dom R holds R.n<=R.(n+1); hence thesis; end; suppose len R = 1; then A2: dom R = {1} by FINSEQ_1:2,def 3; now let n; assume that A3: n in dom R and A4: n+1 in dom R; n = 1 by A2,A3,TARSKI:def 1; hence R.n<=R.(n+1) by A2,A4,TARSKI:def 1; end; hence thesis; end; end; theorem Th17: 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; then n by A1,RFINSEQ:7; A7: n+1 in dom g by A1,A2,A4,FINSEQ_3:25; A8: now A9: rng f = rng g by A3,CLASSES1:75; assume A10: r <> s; now per cases by A10,XXREAL_0:1; case A11: r len f; then ms; r in rng g by A5,A9,FUNCT_1:def 3; then consider m being Nat such that A16: m in dom g and A17: g.m = r by FINSEQ_2:10; A18: m<=len g by A16,FINSEQ_3:25; now per cases; case m = len g; hence contradiction by A1,A2,A15,A17; end; case m <> len g; then m by A1,A2,A8,RFINSEQ:7; now let x be object; card((f|n)"{x}) + card(<*r*>"{x}) = card Coim(f,x) by A6,FINSEQ_3:57 .= card Coim(g,x) by A3,CLASSES1:def 10 .= card((g|n)"{x}) + card(<*r*>"{x}) by A19,FINSEQ_3:57; hence card Coim(f|n,x) = card Coim(g|n,x); end; hence thesis by CLASSES1:def 10; end; theorem Th18: for R be non-decreasing FinSequence of REAL, n be Nat holds R|n is non-decreasing FinSequence of REAL proof let f be non-decreasing FinSequence of REAL, n; set fn = f|n; now per cases; case n = 0; then len fn = 0; hence thesis by Th16; end; case n <> 0; then A1: 0+1<=n by NAT_1:13; now per cases; case len f<=n; hence thesis by FINSEQ_1:58; end; case n = g1 by A3,RFINSEQ:7; len(g1|n) = n by A3,FINSEQ_1:59,NAT_1:11; then g1n = g2n by A2,A3,A4,A5,Lm3; hence thesis by A3,A5,A6,A7,RFINSEQ:7; end; A8: P[0] proof let g1,g2 be non-decreasing FinSequence of REAL; assume len g1 = 0 & g1,g2 are_fiberwise_equipotent; then len g2 = len g1 & g1 = <*>REAL by RFINSEQ:3; hence thesis; end; for m holds P[m] from NAT_1:sch 2(A8,A1); hence thesis; end; theorem Th19: for R1,R2 be non-decreasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds R1 = R2 proof let g1,g2 be non-decreasing FinSequence of REAL; A1: len g1 = len g1; assume g1,g2 are_fiberwise_equipotent; hence thesis by A1,Lm4; end; definition let f be FinSequence of REAL; func sort_a f -> non-decreasing FinSequence of REAL means ::Ascend Sorting or Rearrangement of FinSequences :Def6: f,it are_fiberwise_equipotent; existence by INTEGRA2:3; uniqueness by Th19,CLASSES1:76; projectivity; end; theorem for f being non-increasing FinSequence of REAL holds sort_d f=f by Def5; theorem for f being non-decreasing FinSequence of REAL holds sort_a f=f by Def6; ::\$CT 2 theorem Th22: for f being FinSequence of REAL st f is non-increasing holds -f is non-decreasing proof let f be FinSequence of REAL; assume A1: f is non-increasing; for n being Nat st n in dom (-f) & n+1 in dom (-f) holds (-f) .n <= (-f).(n+1) proof let n be Nat; A2: dom (-f)=dom f by VALUED_1:8; A3: (-f).n=-(f.n) & (-f).(n+1)= -(f.(n+1)) by RVSUM_1:17; assume n in dom (-f) & n+1 in dom (-f); then f.n >= f.(n+1) by A1,A2,RFINSEQ:def 3; hence thesis by A3,XREAL_1:24; end; hence thesis; end; theorem Th23: for f being FinSequence of REAL st f is non-decreasing holds -f is non-increasing proof let f be FinSequence of REAL; assume A1: f is non-decreasing; for n being Nat st n in dom (-f) & n+1 in dom (-f) holds (-f) .n >= (-f).(n+1) proof let n be Nat; A2: dom (-f)=dom f by VALUED_1:8; A3: (-f).n=-(f.n) & (-f).(n+1)= -(f.(n+1)) by RVSUM_1:17; assume n in dom (-f) & n+1 in dom (-f); then f.n <= f.(n+1) by A1,A2; hence thesis by A3,XREAL_1:24; end; hence thesis by RFINSEQ:def 3; end; theorem Th24: for f,g being FinSequence of REAL,P being Permutation of dom g st f = g*P & len g>=1 holds -f=(-g)*P proof let f,g be FinSequence of REAL,P be Permutation of dom g; assume that A1: f = g*P and A2: len g>=1; A3: rng P=dom g by FUNCT_2:def 3; A4: dom (-g)=dom g by VALUED_1:8; then A5: rng ((-g)*P) = rng (-g) by A3,RELAT_1:28; A6: dom (-f)=dom (g*P) by A1,VALUED_1:8; then A7: dom (-f)=dom P by A3,RELAT_1:27; then A8: dom (-f)=dom ((-g)*P) by A3,A4,RELAT_1:27; A9: dom g=Seg len g by FINSEQ_1:def 3; then dom P=dom g by A2,FUNCT_2:def 1; then (-g)*P is FinSequence by A9,A7,A8,FINSEQ_1:def 2; then reconsider k=(-g)*P as FinSequence of REAL by A5,FINSEQ_1:def 4; for i being Nat st i in dom (-f) holds (-f).i=k.i proof let i be Nat; assume A10: i in dom (-f); reconsider j=P.i as Nat; (-f).i=-(f.i) by RVSUM_1:17 .=-(g.(P.i)) by A1,A6,A10,FUNCT_1:12 .=(-g).(j) by RVSUM_1:17 .=((-g)*P).i by A8,A10,FUNCT_1:12; hence thesis; end; hence thesis by A8,FINSEQ_1:13; end; theorem Th25: for f,g being FinSequence of REAL st f,g are_fiberwise_equipotent holds -f,-g are_fiberwise_equipotent proof let f,g be FinSequence of REAL; assume A1: f,g are_fiberwise_equipotent; then consider P being Permutation of dom g such that A2: f = g*P by RFINSEQ:4; A3: now per cases; case len g>=1; hence -f=(-g)*P by A2,Th24; end; case len g<1; then len g<0+1; then A4: len g = 0 by NAT_1:13; then A5: g={}; A6: len f=0 by A1,A4,RFINSEQ:3; then len (-f)=0 by RVSUM_1:114; then A7: -f ={}; f={} by A6; hence -f=(-g)*P by A2,A5,A7; end; end; dom (-g)=dom g by VALUED_1:8; hence thesis by A3,RFINSEQ:4; end; theorem for f being FinSequence of REAL holds sort_d (-f) = - (sort_a f) proof let f be FinSequence of REAL; -f,sort_d(-f) are_fiberwise_equipotent by Def5; then A1: --f,-sort_d(-f) are_fiberwise_equipotent by Th25; -sort_d (-f) is non-decreasing by Th22; then -sort_d (-f)=sort_a f by A1,Def6; hence thesis; end; theorem for f being FinSequence of REAL holds sort_a (-f) = - (sort_d f) proof let f be FinSequence of REAL; -f,sort_a(-f) are_fiberwise_equipotent by Def6; then A1: --f,-sort_a(-f) are_fiberwise_equipotent by Th25; -sort_a (-f) is non-increasing by Th23; then -sort_a (-f)=sort_d f by A1,Def5; hence thesis; end; theorem Th28: for f being FinSequence of REAL holds dom (sort_d f)=dom f & len (sort_d f)=len f proof let f be FinSequence of REAL; f,(sort_d f) are_fiberwise_equipotent by Def5; hence thesis by RFINSEQ:3; end; theorem Th29: for f being FinSequence of REAL holds dom (sort_a f)=dom f & len (sort_a f)=len f proof let f be FinSequence of REAL; f,(sort_a f) are_fiberwise_equipotent by Def6; hence thesis by RFINSEQ:3; end; theorem 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 proof let f be FinSequence of REAL; assume A1: len f>=1; A2: len (sort_d f)=len f by Th28; then 1 in Seg len (sort_d f) by A1,FINSEQ_1:1; then A3: 1 in dom (sort_d f) by FINSEQ_1:def 3; A4: for i being Nat, r1,r2 being Real st i in dom (sort_d f) & r1= (sort_d f).i & r2=(sort_d f).1 holds r1<=r2 proof let i be Nat,r1,r2 be Real; assume that A5: i in dom (sort_d f) and A6: r1=(sort_d f).i & r2=(sort_d f).1; i in Seg len (sort_d f) by A5,FINSEQ_1:def 3; then A7: 1<=i by FINSEQ_1:1; now per cases; case 1=i; hence thesis by A6; end; case 1<>i; then 1=r2 proof let i be Nat,r1,r2 be Real; assume that A11: i in dom (sort_a f) and A12: r1=(sort_a f).i & r2=(sort_a f).1; A13: 1<=i by A11,FINSEQ_3:25; per cases; suppose 1=i; hence thesis by A12; end; suppose 1<>i; then 1