:: Sorting Operators for Finite Sequences
:: by Yatsuka Nakamura
::
:: Received October 17, 2003
:: Copyright (c) 2003-2017 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*