:: Sorting Operators for Finite Sequences
:: by Yatsuka Nakamura
::
:: Received October 17, 2003
:: Copyright (c) 2003-2026 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,
VALUED_0, 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, XXREAL_0, NAT_1, MEMBERED,
FINSEQ_1, 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 real-valued FinSequence;
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 st i in dom f holds f.i <= f.it) &
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 st i<=$1 & i in dom f holds f.i<=f.n) &
(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 st i<=k & i in dom f holds f.i<=f.n1 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 st i<=1 & i in dom f holds f.i<=f.1
proof
let i be Nat;
assume that
A10: i<=1;
assume i in dom f;
then 1<=i by FINSEQ_3:25;
hence thesis by A10,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 st i<=k+1 & i in dom f holds f.i<=f.n1
proof
let i be Nat;
assume that
A17: i<=k+1 and
A18: i in dom f;
per cases;
suppose
i<k+1;
then i<=k by NAT_1:13;
hence thesis by A5,A18;
end;
suppose
i>=k+1;
hence thesis by A15,A17,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;
then j<=k by NAT_1:13;
hence thesis by A6,A23;
end;
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.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 j<=k by NAT_1:13;
hence thesis by A6,A27;
end;
suppose
j>=k+1;
then k<j by NAT_1:13;
hence thesis by A4,A14,XXREAL_0:2;
end;
end;
A28: k>=len f by A25,NAT_1:13;
A29: for i being Nat st i<=k+1 &
i in dom f holds f.i<=f.n1
proof
let i be Nat;
assume that
i<=k+1 and
A30: i in dom f;
i<=len f by A1,A30,FINSEQ_1:1;
then i<=k by A28,XXREAL_0:2;
hence thesis by A5,A30;
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 st i<=k+1 & i in dom f holds f.i<=f.n2
proof
let i be Nat;
assume that
A34: i<=k+1 and
A35: i in dom f;
set r1=f.i;
per cases;
suppose
A38: i<k+1;
reconsider r3=f.n1 as Real;
i<=k by A38,NAT_1:13;
then r1<=r3 by A5,A35;
hence thesis by A24,XXREAL_0:2;
end;
suppose
i>=k+1;
hence thesis by A34,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;
then j<=k by NAT_1:13;
hence thesis by A5,A24,A40;
end;
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 st i<=0 & i in dom f holds f.i<=f.1)&
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 st i<=len f & i in dom f holds f.i<=f.n1 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 st i in dom f holds f.i<=f.n1
proof
let i be Nat;
assume
A48: i in dom f;
then i<=len f by FINSEQ_3:25;
hence thesis by A43,A48;
end;
hence thesis by A2,A42,A45;
end;
end;
uniqueness
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 st i in dom f holds f.i<=f.m1) &
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 st i in dom f holds f.i<=f.m2) & 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;
definition
let f be real-valued FinSequence;
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 st i in dom f holds f.i >= f.it) &
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 st i<=$1 & i in dom f
holds f.i>=f.n) & (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 st i<=k & i in dom f holds f.i>=f.n1 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 st i<=1 & i in dom f holds f.i>=f.1
proof
let i be Nat;
assume that
A10: i<=1 and
A11: i in dom f;
1<=i by A11,FINSEQ_3:25;
hence thesis by A10,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 st i<=k+1 & i in dom f holds f.i>=f.n1
proof
let i be Nat;
assume that
A17: i<=k+1 and
A18: i in dom f;
per cases;
suppose
i<k+1;
then i<=k by NAT_1:13;
hence thesis by A5,A18;
end;
suppose
i>=k+1;
hence thesis by A15,A17,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;
then j<=k by NAT_1:13;
hence thesis by A6,A23;
end;
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 j<=k by NAT_1:13;
hence thesis by A6,A27;
end;
suppose
j>=k+1;
then k<j by NAT_1:13;
hence thesis by A4,A14,XXREAL_0:2;
end;
end;
A28: k>=len f by A25,NAT_1:13;
A29: for i being Nat st i<=k+1 & i in dom f holds f.i>=f.n1
proof
let i be Nat;
assume that
i<=k+1 and
A30: i in dom f;
i<=len f by A1,A30,FINSEQ_1:1;
then i<=k by A28,XXREAL_0:2;
hence thesis by A5,A30;
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 st i<=k+1 & i in dom f holds f.i>=f.n2
proof
let i be Nat;
assume that
A34: i<=k+1 and
A35: i in dom f;
set r1=f.i;
per cases;
suppose
A38: i<k+1;
reconsider r3=f.n1 as Real;
i<=k by A38,NAT_1:13;
then r1>=r3 by A5,A35;
hence thesis by A24,XXREAL_0:2;
end;
suppose
i>=k+1;
hence thesis by A34,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;
then j<=k by NAT_1:13;
hence thesis by A5,A24,A40;
end;
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 st i<=0 & i in dom f holds f.i>=f.1)&
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 st i<=len f & i in dom f holds f.i>=f.n1 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 st i in dom f holds f.i>=f.n1
proof
let i be Nat;
assume
A48: i in dom f;
i<=len f by A48,FINSEQ_3:25;
hence thesis by A43,A48;
end;
hence thesis by A2,A42,A45;
end;
end;
hence thesis;
end;
uniqueness
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 st i in dom f holds f.i
>=f.m1) & 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
st i in dom f holds f.i>=f.m2) & 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;
definition
let f be real-valued FinSequence;
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 real-valued FinSequence,i being Nat st
1<=i & i<=len f holds f.i<=f.(max_p f) & f.i<=max f
proof
let f be real-valued FinSequence,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 real-valued FinSequence,i being Nat st
1<=i & i<=len f holds f.i>=f.(min_p f) & f.i>=min f
proof
let f be real-valued FinSequence,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 real-valued FinSequence,r being Real st
f=<*r*> holds max_p f= 1 & max f=r
proof
let f be real-valued FinSequence,r be Real;
assume
A1: f=<*r*>;
then
A2: f.1=r;
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 real-valued FinSequence,r being Real st
f=<*r*> holds min_p f= 1 & min f=r
proof
let f be real-valued FinSequence,r be Real;
assume
A1: f=<*r*>;
then
A2: f.1=r;
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 real-valued FinSequence,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 real-valued FinSequence,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;
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;
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 max_p f <1+1 by A1,FINSEQ_1:44;
then max_p f <=1 by NAT_1:13;
then
A11: max_p f=1 by A6,XXREAL_0:1;
then max f <=max(r1,r2) by A4,XXREAL_0:25;
then max f=max(r1,r2) by A10,XXREAL_0:1;
hence thesis by A4,A11,FUNCOP_1:def 8;
end;
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<r2;
then
A14: max(r1,r2)<=max f by A8,A3,XXREAL_0:def 10;
now
per cases;
case
max_p f<len f;
then max_p f <1+1 by A1,FINSEQ_1:44;
then max_p f <=1 by NAT_1:13;
then
A15: max_p f=1 by A6,XXREAL_0:1;
then max f <=max(r1,r2) by A4,XXREAL_0:25;
then max f=max(r1,r2) by A14,XXREAL_0:1;
hence thesis by A4,A15,FUNCOP_1:def 8;
end;
case
max_p f>=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 real-valued FinSequence,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 real-valued FinSequence,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;
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;
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<len f;
then min_p f <1+1 by A1,FINSEQ_1:44;
then min_p f <=1 by NAT_1:13;
then
A11: min_p f=1 by A6,XXREAL_0:1;
then min 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<len f;
then min_p f <1+1 by A1,FINSEQ_1:44;
then min_p f <=1 by NAT_1:13;
then
A15: min_p f=1 by A6,XXREAL_0:1;
then min 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 real-valued FinSequence st len f1=len f2 & len f1>0 holds
max (f1+f2)<=(max f1) +(max f2)
proof
let f1,f2 be real-valued FinSequence;
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 real-valued FinSequence st len f1=len f2 & len f1>0 holds
min (f1+f2)>=(min f1) +(min f2)
proof
let f1,f2 be real-valued FinSequence;
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 real-valued FinSequence, 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 real-valued FinSequence, 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 real-valued FinSequence, 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 real-valued FinSequence, 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 real-valued FinSequence st len f>0 holds
max (-f)=-(min f) & max_p (-f)=min_p f
proof
let f be real-valued FinSequence;
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 real-valued FinSequence st len f>0 holds
min (-f)=-(max f) & min_p (-f)=max_p f
proof
let f be real-valued FinSequence;
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<len f
holds max (f/^n)<= max f & min (f/^n)>= min f
proof
let f be FinSequence of REAL,n be Nat;
A1: 1<=1+n by NAT_1:12;
assume
A2: n<len f;
then
A3: len (f/^n)=len f -n by RFINSEQ:def 1;
then
A4: len (f/^n)>0 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 real-valued FinSequence st f,g are_fiberwise_equipotent
holds max f<=max g
proof
let f,g be real-valued FinSequence;
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 real-valued FinSequence st
f,g are_fiberwise_equipotent holds max f=max g
proof
let f,g be real-valued FinSequence;
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 real-valued FinSequence st f,g are_fiberwise_equipotent
holds min f>=min g
proof
let f,g be real-valued FinSequence;
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 real-valued FinSequence st
f,g are_fiberwise_equipotent holds min f=min g
proof
let f,g be real-valued FinSequence;
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 real-valued FinSequence;
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 real-valued FinSequence st len R = 0 or len R = 1 holds
R is non-decreasing FinSequence of REAL
proof
let R be real-valued FinSequence;
assume
A1: len R = 0 or len R = 1;
reconsider R as FinSequence of REAL by RVSUM_1:145;
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 by INTEGRA2:def 1;
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 by INTEGRA2:def 1;
end;
end;
theorem Th17:
for R be real-valued FinSequence 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
proof
let R be real-valued FinSequence;
thus R is non-decreasing implies for n,m st n in dom R & m in dom R & n<m
holds R.n<=R.m
proof
defpred P[Nat] means $1 in dom R implies for n st n in dom R &
n<$1 holds R.n<=R.$1;
assume
A1: R is non-decreasing;
A2: for m st P[m] holds P[m+1]
proof
let m;
assume
A3: P[m];
assume
A4: m+1 in dom R;
then m+1<=len R by FINSEQ_3:25;
then
A5: m<=len R by NAT_1:13;
let n;
assume that
A6: n in dom R and
A7: n<m+1;
set t = R.m, r = R.n, s = R.(m+1);
A8: n<=m by A7,NAT_1:13;
1<=n by A6,FINSEQ_3:25;
then
A9: 1<=m by A8,XXREAL_0:2;
then
A10: m in dom R by A5,FINSEQ_3:25;
now
per cases;
case
n = m;
hence thesis by A1,A4,A6;
end;
case
n <> m;
then n<m by A8,XXREAL_0:1;
then
A11: r<=t by A3,A6,A9,A5,FINSEQ_3:25;
t<=s by A1,A4,A10;
hence thesis by A11,XXREAL_0:2;
end;
end;
hence thesis;
end;
A12: P[0];
for m holds P[m] from NAT_1:sch 2(A12,A2);
hence thesis;
end;
assume
A13: for n,m st n in dom R & m in dom R & n<m holds R.n<=R.m;
let n;
A14: n<n+1 by NAT_1:13;
assume n in dom R & n+1 in dom R;
hence thesis by A13,A14;
end;
Lm3: for f,g be non-decreasing real-valued FinSequence, n 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
let f,g be non-decreasing real-valued FinSequence, n;
assume that
A1: len f = n+1 and
A2: len f = len g and
A3: f,g are_fiberwise_equipotent;
set r = f.(n+1), s = g.(n+1);
A4: 0+1<=n+1 by NAT_1:13;
then
A5: n+1 in dom f by A1,FINSEQ_3:25;
A6: f = (f|n)^<*r*> 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<s;
s in rng f by A7,A9,FUNCT_1:def 3;
then consider m being Nat such that
A12: m in dom f and
A13: f.m = s by FINSEQ_2:10;
A14: m<=len f by A12,FINSEQ_3:25;
now
per cases;
case
m = len f;
hence contradiction by A1,A11,A13;
end;
case
m <> len f;
then m<n+1 by A1,A14,XXREAL_0:1;
hence contradiction by A5,A11,A12,A13,Th17;
end;
end;
hence contradiction;
end;
case
A15: r>s;
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<n+1 by A1,A2,A18,XXREAL_0:1;
hence contradiction by A7,A15,A16,A17,Th17;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence f.(len f) = g.(len g) by A1,A2;
A19: g = (g|n)^<*r*> 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 real-valued FinSequence, n be Nat
holds R|n is non-decreasing FinSequence of REAL
proof
let f be non-decreasing real-valued FinSequence, n;
reconsider f as non-decreasing FinSequence of REAL by RVSUM_1:145;
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<len f;
then
A2: n in dom f & len fn = n by A1,FINSEQ_1:59,FINSEQ_3:25;
now
let m;
A3: dom fn = Seg len fn by FINSEQ_1:def 3;
assume
A4: m in dom fn & m+1 in dom fn;
then
A5: m in dom f & m+1 in dom f by A2,A3,RFINSEQ:6;
f.m = fn.m & f.(m+1) = fn.(m+1) by A2,A4,A3,RFINSEQ:6;
hence fn.m<=fn.(m+1) by A5,INTEGRA2:def 1;
end;
hence thesis by INTEGRA2:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm4: for n holds for g1,g2 be non-decreasing real-valued FinSequence st
n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2
proof
defpred P[Nat] means for g1,g2 be non-decreasing real-valued FinSequence
st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let g1,g2 be non-decreasing real-valued FinSequence;
set r = g1.(n+1);
reconsider g1n = g1|n, g2n = g2|n as non-decreasing FinSequence of REAL
by Th18;
assume that
A3: len g1 = n+1 and
A4: g1,g2 are_fiberwise_equipotent;
A5: len g2 = len g1 by A4,RFINSEQ:3;
then
A6: g1.(len g1) = g2.(len g2) by A3,A4,Lm3;
A7: (g1|n)^<*r*> = 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 real-valued FinSequence;
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 real-valued FinSequence st
R1,R2 are_fiberwise_equipotent holds R1 = R2
proof
let g1,g2 be non-decreasing real-valued FinSequence;
len g1 = len g1;
hence thesis by Lm4;
end;
definition
let f be real-valued FinSequence;
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 real-valued FinSequence holds sort_d f = f
proof
let f be non-increasing real-valued FinSequence;
f is FinSequence of REAL by RVSUM_1:145;
hence thesis by Def5;
end;
theorem
for f being non-decreasing real-valued FinSequence holds sort_a f = f
proof
let f be non-decreasing real-valued FinSequence;
f is FinSequence of REAL by RVSUM_1:145;
hence thesis by Def6;
end;
::$CT 2
theorem Th22:
for f being real-valued FinSequence st
f is non-increasing holds -f is non-decreasing
proof
let f be real-valued FinSequence;
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 real-valued FinSequence st
f is non-decreasing holds -f is non-increasing
proof
let f be real-valued FinSequence;
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 real-valued FinSequence,P being Permutation of dom g
st f = g*P & len g>=1 holds -f=(-g)*P
proof
let f,g be real-valued FinSequence,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 real-valued FinSequence st
f,g are_fiberwise_equipotent holds -f,-g are_fiberwise_equipotent
proof
let f,g be real-valued FinSequence;
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 real-valued FinSequence holds sort_d (-f) = - (sort_a f)
proof
let f be real-valued FinSequence;
-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 real-valued FinSequence holds sort_a (-f) = - (sort_d f)
proof
let f be real-valued FinSequence;
-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 real-valued FinSequence holds
dom (sort_d f)=dom f & len (sort_d f)=len f
proof
let f be real-valued FinSequence;
f,(sort_d f) are_fiberwise_equipotent by Def5;
hence thesis by RFINSEQ:3;
end;
theorem Th29:
for f being real-valued FinSequence holds
dom (sort_a f)=dom f & len (sort_a f)=len f
proof
let f be real-valued FinSequence;
f,(sort_a f) are_fiberwise_equipotent by Def6;
hence thesis by RFINSEQ:3;
end;
theorem
for f being real-valued FinSequence 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 real-valued FinSequence;
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 st i in dom (sort_d f) holds (sort_d f).i<=(sort_d f).1
proof
let i be Nat;
assume
A5: i in dom (sort_d f);
set r1=(sort_d f).i;
set 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;
end;
case
1<>i;
then 1<i by A7,XXREAL_0:1;
hence thesis by A3,A5,RFINSEQ:19;
end;
end;
hence thesis;
end;
A8: len (sort_a f)=len f by Th29;
then
A9: 1 in dom (sort_a f) by A1,FINSEQ_3:25;
A10: for i being Nat st i in dom (sort_a f) holds (sort_a f).i>=(sort_a f).1
proof
let i be Nat;
assume that
A11: i in dom (sort_a f);
set r1=(sort_a f).i;
set r2=(sort_a f).1;
A13: 1<=i by A11,FINSEQ_3:25;
per cases;
suppose
1=i;
hence thesis;
end;
suppose
1<>i;
then 1<i by A13,XXREAL_0:1;
hence thesis by A9,A11,Th17;
end;
end;
A14: f,(sort_a f) are_fiberwise_equipotent by Def6;
A15: f,(sort_d f) are_fiberwise_equipotent by Def5;
A16: for j being Nat st j in dom (sort_a f) & (sort_a f).j=(
sort_a f).1 holds 1<=j by FINSEQ_3:25;
then
A17: (sort_a f).1=min (sort_a f) by A1,A8,A9,A10,Def2
.=min f by A14,Th15;
A18: for j being Nat st j in dom (sort_d f) & (sort_d f).j=(
sort_d f).1 holds 1<=j
proof
let j be Nat;
assume that
A19: j in dom (sort_d f) and
(sort_d f).j=(sort_d f).1;
j in Seg len (sort_d f) by A19,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:1;
end;
then (sort_d f).1=max (sort_d f) by A1,A2,A3,A4,Def1
.=max f by A15,Th14;
hence thesis by A1,A2,A3,A4,A18,A8,A9,A10,A16,A17,Def1,Def2;
end;