Copyright (c) 2003 Association of Mizar Users
environ
vocabulary RELAT_1, CARD_1, FUNCT_1, BOOLE, FUNCT_2, FINSEQ_1, ARYTM_1,
SQUARE_1, PROB_1, RFINSEQ, RFINSEQ2, CQC_LANG;
notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
FINSEQ_1, CARD_1, REAL_1, NAT_1, SQUARE_1, SEQ_1, RVSUM_1, TOPREAL1,
CQC_LANG, RFINSEQ, INTEGRA2;
constructors REAL_1, NAT_1, SQUARE_1, TOPREAL1, SEQ_1, CQC_LANG, RFINSEQ,
INTEGRA2;
clusters NUMBERS, FUNCT_1, RELSET_1, FINSEQ_1, XREAL_0, FUNCT_2, REAL_1,
NAT_1, RFINSEQ, INTEGRA2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions INTEGRA2;
theorems AXIOMS, TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, REAL_1, NAT_1, FUNCT_1,
FUNCT_2, SQUARE_1, TOPREAL1, RVSUM_1, RELAT_1, XCMPLX_1, CQC_LANG,
EUCLID_2, RFINSEQ, XBOOLE_0, INTEGRA2;
schemes NAT_1;
begin
reserve n,m for Nat;
definition let f be FinSequence of REAL;
func max_p f -> Nat means
:AA10: (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
Na: dom f=Seg len f by FINSEQ_1:def 3;
per cases;
suppose len f=0;
hence ex n being Nat st
(len f=0 implies n=0) & (len f>0 implies n in dom f &
(for i be Nat,r1,r2 be Real st i in dom f & r1=f.i & r2=f.n
holds r1<=r2) & (for j being Nat st j in dom f & f.j=f.n holds n<=j));
suppose Ka: 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));
Mu: for i being Nat,r1,r2 being Real st i<=0 & i in dom f
& r1=f.i & r2=f.1 holds r1<=r2
proof let i be Nat,r1,r2 be Real;
assume Ra: i<=0 & i in dom f
& r1=f.i & r2=f.1;
1<=i & i<=len f by Na,Ra,FINSEQ_1:3;
hence r1<=r2 by Ra,AXIOMS:22;
end;
for j being Nat st j<=0 & j in dom f & f.j=f.1 holds 1<=j by FINSEQ_3:27;
then
Ji: P[0] by Mu;
Bo: 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
Rn: (k<>0 implies n1<=k & n1 in dom f) &
(for i being Nat,r1,r2 being Real st i<=k & i in dom f
& r1=f.i & r2=f.n1
holds r1<=r2) & (for j being Nat st j<=k & j in dom f & f.j=f.n1
holds n1<=j);
per cases;
suppose On: k=0;
Ap: dom f=Seg len f by FINSEQ_1:def 3;
len f>0 by NAT_1:19,Ka;then
len f>=0+1 by NAT_1:38;then
Ri: 1<=1 & 1 in dom f by Ap,FINSEQ_1:3;
L12: 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 Cm19: i<=1 & i in dom f & r1=f.i & r2=f.1;then
1<=i & i<=len f by FINSEQ_3:27;
hence r1<=r2 by Cm19,AXIOMS:21;
end;
for j being Nat st j<=1 & j in dom f & f.j=f.1
holds 1<=j by Ap,FINSEQ_1:3;
hence P[k+1] by On,Ri,L12;
suppose F74: k<>0;
now per cases;
case So: f.n1>=f.(k+1);
fY: n1<=k+1 by Rn,F74,NAT_1:38;
AT: k+1<>0 implies n1<=k+1 & n1 in dom f by Rn,F74,NAT_1:38;
UT: 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 TU: i<=k+1 & i in dom f
& r1=f.i & r2=f.n1;
per cases;
suppose i<k+1;then i<=k by NAT_1:38;
hence r1<=r2 by Rn,TU;
suppose i>=k+1;
hence r1<=r2 by TU,So,AXIOMS:21;
end;
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 KA: j<=k+1 & j in dom f & f.j=f.n1;
now per cases;
case j<k+1;then j<=k by NAT_1:38;
hence n1<=j by Rn,KA;
case j>=k+1;
hence n1<=j by fY,KA,AXIOMS:21;
end;
hence n1<=j;
end;
hence P[k+1] by AT,UT;
case NA: f.n1<f.(k+1);
now per cases;
case KA: k+1>len f;then
MU: k>=len f by NAT_1:38;
1<=n1 & n1<=len f by F74,Rn,FINSEQ_1:3,Na;then
L3: k+1<>0 implies n1<=k+1 & n1 in dom f by KA,Rn,AXIOMS:22;
L4: 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 M1: i<=k+1 & i in dom f
& r1=f.i & r2=f.n1;then
1<=i & i<=len f by FINSEQ_1:3,Na;then
i<=k by MU,AXIOMS:22;
hence r1<=r2 by Rn,M1;
end;
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 M1: j<=k+1 & j in dom f & f.j=f.n1;
per cases;
suppose j<k+1;then
j<=k by NAT_1:38;
hence n1<=j by Rn,M1;
suppose j>=k+1;then
k<j by NAT_1:38;
hence n1<=j by Rn,F74,AXIOMS:22;
end;
hence P[k+1] by L3,L4;
case J5: k+1<=len f;
j6: 1<=1+k by NAT_1:37;
set n2=k+1;
J7: (k+1<>0 implies n2<=k+1 &
n2 in dom f) by j6,Na,J5,FINSEQ_1:3;
E4: 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 H1: i<=k+1 & i in dom f & r1=f.i & r2=f.n2;
per cases;
suppose i<k+1;then
J11: i<=k by NAT_1:38;
reconsider r3=f.n1 as Real;
r1<=r3 by Rn,H1,J11;
hence r1<=r2 by NA,H1,AXIOMS:22;
suppose i>=k+1;
hence r1<=r2 by H1,AXIOMS:21;
end;
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 J2: j<=k+1 & j in dom f & f.j=f.n2;
per cases;
suppose j<k+1;then
j<=k by NAT_1:38;
hence n2<=j by J2,Rn,NA;
suppose j>=k+1;
hence n2<=j;
end;
hence P[k+1] by J7,E4;
end;
hence P[k+1];
end;
hence P[k+1];
end;
for k being Nat holds P[k] from Ind(Ji,Bo);then
consider n1 being Nat such that
A7: (len f<>0 implies n1<=len f &
n1 in dom f) &
(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) & (for j being Nat st j<=len f & j in dom f & f.j=f.n1
holds n1<=j);
A8: 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 C1: i in dom f & r1=f.i & r2=f.n1;then
1<=i & i<=len f by FINSEQ_3:27;
hence r1<=r2 by C1,A7;
end;
for j being Nat st j in dom f & f.j=f.n1 holds n1<=j
proof let j be Nat;
assume D1: j in dom f & f.j=f.n1;then
1<=j & j<=len f by FINSEQ_3:27;
hence n1<=j by D1,A7;
end;
hence ex n being Nat st
(len f=0 implies n=0) &
(len f>0 implies n in dom f &
(for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.n
holds r1<=r2) & (for j being Nat st j in dom f & f.j=f.n holds n<=j))
by Ka,A7,A8;
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 B1: ((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)));
B6: f.m2<=f.m1 by B1,NAT_1:19;
f.m1<=f.m2 by B1,NAT_1:19;then
B8: f.m1=f.m2 by B6,AXIOMS:21;
B9: m1<=m2 by B8,B1,NAT_1:19;
m2<=m1 by B8,B1,NAT_1:19;
hence m1=m2 by B9,AXIOMS:21;
end;
end;
end;
definition let f be FinSequence of REAL;
func min_p f -> Nat means
:AA20: (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
K1: dom f=Seg len f by FINSEQ_1:def 3;
now per cases;
case len f=0;
hence ex n being Nat st
(len f=0 implies n=0) & (len f>0 implies n in dom f &
(for i be Nat,r1,r2 be Real st i in dom f & r1=f.i & r2=f.n
holds r1>=r2) & (for j being Nat st j in dom f & f.j=f.n holds n<=j));
case B0: 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));
A2: for i being Nat,r1,r2 being Real st i<=0 & i in dom f
& r1=f.i & r2=f.1
holds r1>=r2
proof let i be Nat,r1,r2 be Real;
assume B1: i<=0 & i in dom f
& r1=f.i & r2=f.1;
1<=i & i<=len f by K1,B1,FINSEQ_1:3;
hence r1>=r2 by B1,AXIOMS:22;
end;
for j being Nat st j<=0 & j in dom f & f.j=f.1
holds 1<=j by FINSEQ_3:27;then
A3: P[0] by A2;
A4: 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
E2: (k<>0 implies n1<=k &
n1 in dom f) &
(for i being Nat,r1,r2 being Real st i<=k & i in dom f
& r1=f.i & r2=f.n1
holds r1>=r2) & (for j being Nat st j<=k & j in dom f & f.j=f.n1
holds n1<=j);
now per cases;
case F9: k=0;
F0: dom f=Seg len f by FINSEQ_1:def 3;
len f>0 by NAT_1:19,B0;then
len f>=0+1 by NAT_1:38;then
F1: 1<=1 & 1 in dom f by F0,FINSEQ_1:3;
F2: 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 G1: i<=1 & i in dom f
& r1=f.i & r2=f.1;then
1<=i & i<=len f by FINSEQ_3:27;
hence r1>=r2 by G1,AXIOMS:21;
end;
for j being Nat st j<=1 & j in dom f & f.j=f.1
holds 1<=j by F0,FINSEQ_1:3;
hence P[k+1] by F9,F1,F2;
case F9: k<>0;
now per cases;
case J0: f.n1<=f.(k+1);
E8: n1<=k+1 by E2,F9,NAT_1:38;
E3: k+1<>0 implies n1<=k+1 & n1 in dom f by E2,F9,NAT_1:38;
E4: 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 H1: i<=k+1 & i in dom f & r1=f.i & r2=f.n1;
per cases;
suppose i<k+1;then i<=k by NAT_1:38;
hence r1>=r2 by E2,H1;
suppose i>=k+1;
hence r1>=r2 by H1,J0,AXIOMS:21;
end;
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 J2: j<=k+1 & j in dom f & f.j=f.n1;
per cases;
suppose j<k+1;then j<=k by NAT_1:38;
hence n1<=j by E2,J2;
suppose j>=k+1;
hence n1<=j by E8,J2,AXIOMS:21;
end;
hence P[k+1] by E3,E4;
case J0: f.n1>f.(k+1);
now per cases;
case L1: k+1>len f;then
L5: k>=len f by NAT_1:38;
1<=n1 & n1<=len f by F9,E2,FINSEQ_1:3,K1;then
L3: k+1<>0 implies n1<=k+1 & n1 in dom f by L1,E2,AXIOMS:22;
L4: 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 M1: i<=k+1 & i in dom f
& r1=f.i & r2=f.n1;then
1<=i & i<=len f by FINSEQ_1:3,K1;then
i<=k by L5,AXIOMS:22;
hence r1>=r2 by E2,M1;
end;
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 M1: j<=k+1 & j in dom f & f.j=f.n1;
per cases;
suppose j<k+1;then
j<=k by NAT_1:38;
hence n1<=j by E2,M1;
suppose j>=k+1;then
k<j by NAT_1:38;
hence n1<=j by E2,F9,AXIOMS:22;
end;
hence P[k+1] by L3,L4;
case J5: k+1<=len f;
j6: 1<=1+k by NAT_1:37;
set n2=k+1;
J7: (k+1<>0 implies n2<=k+1 &
n2 in dom f) by j6,K1,J5,FINSEQ_1:3;
E4: 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 H1: i<=k+1 & i in dom f & r1=f.i & r2=f.n2;
per cases;
suppose i<k+1;then
J11: i<=k by NAT_1:38;
reconsider r3=f.n1 as Real;
r1>=r3 by E2,H1,J11;
hence r1>=r2 by J0,H1,AXIOMS:22;
suppose i>=k+1;
hence r1>=r2 by H1,AXIOMS:21;
end;
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 J2: j<=k+1 & j in dom f & f.j=f.n2;
per cases;
suppose j<k+1;then
j<=k by NAT_1:38;
hence n2<=j by J2,E2,J0;
suppose j>=k+1;
hence n2<=j;
end;
hence P[k+1] by J7,E4;
end;
hence P[k+1];
end;
hence P[k+1];
end;
hence P[k+1];
end;
for k being Nat holds P[k] from Ind(A3,A4);then
consider n1 being Nat such that
A7: (len f<>0 implies n1<=len f & n1 in dom f) &
(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) & (for j being Nat st j<=len f & j in dom f & f.j=f.n1
holds n1<=j);
A8: 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 C1: i in dom f & r1=f.i & r2=f.n1;then
1<=i & i<=len f by FINSEQ_3:27;
hence r1>=r2 by C1,A7;
end;
for j being Nat st j in dom f & f.j=f.n1 holds n1<=j
proof let j be Nat;
assume D1: j in dom f & f.j=f.n1;then
1<=j & j<=len f by FINSEQ_3:27;
hence n1<=j by D1,A7;
end;
hence ex n being Nat st (len f=0 implies n=0) &
(len f>0 implies n in dom f &
(for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.n
holds r1>=r2) & (for j being Nat st j in dom f & f.j=f.n holds n<=j))
by B0,A7,A8;
end;
hence ex n being Nat st
(len f=0 implies n=0) & (len f>0 implies n in dom f &
(for i be Nat,r1,r2 be Real st i in dom f & r1=f.i & r2=f.n
holds r1>=r2) & (for j being Nat st j in dom f & f.j=f.n holds n<=j));
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 B1: ((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)));
per cases;
suppose len f=0;
hence m1=m2 by B1;
suppose b3:len f<>0;
B4b: for i being Nat,r1,r2 being Real st i in dom f & r1=f.i & r2=f.m2
holds r1>=r2 by B1,b3,NAT_1:19;
B5: m1 in dom f by B1,b3,NAT_1:19;
B6: f.m2>=f.m1 by B1,NAT_1:19;
f.m1>=f.m2 by B4b,B5;then
B8: f.m1=f.m2 by B6,AXIOMS:21;
B9: m1>=m2 by B8,B1,NAT_1:19;
m2>=m1 by B8,B1,NAT_1:19;
hence m1=m2 by B9,AXIOMS:21;
end;
end;
end;
definition let f be FinSequence of REAL;
func max f -> Real equals
:AA30: f.(max_p f);
correctness;
func min f -> Real equals
:AA40: f.(min_p f);
correctness;
end;
theorem BB10: 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:27;
0<len f by AXIOMS:22,A1;
hence f.i<=f.(max_p f) by A2,AA10;
hence f.i<=max f by AA30;
end;
theorem BB20: 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:27;
0<len f by AXIOMS:22,A1;
hence f.i>=f.(min_p f) by A2,AA20;
hence f.i>=min f by AA40;
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 f=<*r*>;then
A2: len f=1 & f.1=r by FINSEQ_1:57;then
(max_p f) in dom f by AA10;then
1<= (max_p f) & (max_p f)<=len f by FINSEQ_3:27;then
max_p f=1 by A2,AXIOMS:21;
hence max_p f=1 & max f=r by AA30,A2;
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 f=<*r*>;then
A2: len f=1 & f.1=r by FINSEQ_1:57;then
(min_p f) in dom f by AA20;then
1<= (min_p f) & (min_p f)<=len f by FINSEQ_3:27;then
min_p f=1 by A2,AXIOMS:21;
hence min_p f=1 & min f=r by AA40,A2;
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 f=<*r1,r2*>;then
A2: len f=2 & f.1=r1 & f.2=r2 by FINSEQ_1:61;then
(max_p f) in dom f by AA10;then
A4: 1<= (max_p f) & (max_p f)<=len f by FINSEQ_3:27;
A3: f.1<=f.(max_p f) & f.1<=max f by A2,BB10;
A3b: f.2<=f.(max_p f) & f.2<=max f by BB10,A2;
now per cases;
case r1>=r2;then
B1: max(r1,r2)<=max f by A3,A2,SQUARE_1:def 2;
B2: max f=f.(max_p f) by AA30;
now per cases;
case max_p f<len f;then max_p f <1+1 by A2;then
max_p f <=1 by NAT_1:38;then
C3: max_p f=1 by A4,AXIOMS:21;then
max f=r1 by B2,A2;then
max f <=max(r1,r2) by SQUARE_1:46;then
max f=max(r1,r2) by B1,AXIOMS:21;
hence max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2)
by C3,B2,A2,CQC_LANG:def 1;
case max_p f>=len f;then
C3: max_p f=2 by A4,A2,AXIOMS:21;then
C1: max f=r2 by B2,A2;
C4: 1 in dom f by A2,FINSEQ_3:27;
C5: r1<>r2 by A2,AA10,C3,C4;
max f <=max(r1,r2) by C1,SQUARE_1:46;then
max f=max(r1,r2) by B1,AXIOMS:21;
hence max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2)
by C3,C5,B2,A2,CQC_LANG:def 1;
end;
hence max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2);
case r1<r2;then
B1: max(r1,r2)<=max f by A3b,A2,SQUARE_1:def 2;
B2: max f=f.(max_p f) by AA30;
now per cases;
case max_p f<len f;then max_p f <1+1 by A2;then
max_p f <=1 by NAT_1:38;then
C3: max_p f=1 by A4,AXIOMS:21;then
C1: max f=r1 by B2,A2;then
max f <=max(r1,r2) by SQUARE_1:46;then
max f=max(r1,r2) by B1,AXIOMS:21;
hence max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2)
by C3,C1,CQC_LANG:def 1;
case max_p f>=len f;then
C3: max_p f=2 by A4,A2,AXIOMS:21;
C4: 1 in dom f by A2,FINSEQ_3:27;
C5: r1<>r2 by A2,AA10,C3,C4;
max f <=max(r1,r2) by C3,B2,A2,SQUARE_1:46;then
max f=max(r1,r2) by B1,AXIOMS:21;
hence max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2)
by C3,C5,B2,A2,CQC_LANG:def 1;
end;
hence max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2);
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 f=<*r1,r2*>;then
A2: len f=2 & f.1=r1 & f.2=r2 by FINSEQ_1:61;then
(min_p f) in dom f by AA20;then
A4: 1<= (min_p f) & (min_p f)<=len f by FINSEQ_3:27;
A3: f.1>=f.(min_p f) & f.1>=min f by A2,BB20;
A3b: f.2>=f.(min_p f) & f.2>=min f by BB20,A2;
per cases;
suppose r1<=r2;then
B1: min(r1,r2)>=min f by A3,A2,SQUARE_1:def 1;
B2: min f=f.(min_p f) by AA40;
now per cases;
case min_p f<len f;then min_p f <1+1 by A2;then
min_p f <=1 by NAT_1:38;then
C3: min_p f=1 by A4,AXIOMS:21;then
C1: min f=r1 by B2,A2;then
min f >=min(r1,r2) by SQUARE_1:35;then
min f=min(r1,r2) by B1,AXIOMS:21;
hence min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2)
by C3,C1,CQC_LANG:def 1;
case min_p f>=len f;then
C3: min_p f=2 by A4,A2,AXIOMS:21;
C4: 1 in dom f by A2,FINSEQ_3:27;
C5: r1<>r2 by A2,AA20,C3,C4;
min f >=min(r1,r2) by C3,B2,A2,SQUARE_1:35;then
min f=min(r1,r2) by B1,AXIOMS:21;
hence min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2)
by C3,C5,B2,A2,CQC_LANG:def 1;
end;
hence min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2);
suppose r1>r2;then
B1: min(r1,r2)>=min f by A3b,A2,SQUARE_1:def 1;
B2: min f=f.(min_p f) by AA40;
now per cases;
case min_p f<len f;then min_p f <1+1 by A2;then
min_p f <=1 by NAT_1:38;then
C3: min_p f=1 by A4,AXIOMS:21;then
min f=r1 by B2,A2;then
min f >=min(r1,r2) by SQUARE_1:35;then
min f=min(r1,r2) by B1,AXIOMS:21;
hence min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2)
by C3,B2,A2,CQC_LANG:def 1;
case min_p f>=len f;then
C3: min_p f=2 by A4,A2,AXIOMS:21;then
C1: min f=r2 by B2,A2;
C4: 1 in dom f by A2,FINSEQ_3:27;
C5: r1<>r2 by A2,AA20,C3,C4;
min f >=min(r1,r2) by C1,SQUARE_1:35;then
min f=min(r1,r2) by B1,AXIOMS:21;
hence min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2)
by C3,C5,C1,CQC_LANG:def 1;
end;
hence thesis;
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 A1: len f1=len f2 & len f1>0;then
A4: len (f1+f2)=len f1 by EUCLID_2:6;
A11: max_p (f1+f2) in dom (f1+f2) by A4,A1,AA10;then
A3: 1<=max_p (f1+f2) & max_p (f1+f2)<=len (f1+f2) by FINSEQ_3:27;
A10: max (f1+f2)=(f1+f2).(max_p (f1+f2)) by AA30
.=f1.(max_p (f1+f2)) + f2.(max_p (f1+f2)) by RVSUM_1:26,A11;
A5: max_p (f1+f2) in Seg len f1 by FINSEQ_1:3,A3,A4;then
max_p (f1+f2) in dom f1 by FINSEQ_1:def 3;then
A6: f1.(max_p (f1+f2))<=f1.(max_p f1) by AA10,A1;
A7: f1.(max_p f1)=max f1 by AA30;
max_p (f1+f2) in dom f2 by A5,A1,FINSEQ_1:def 3;then
A8: f2.(max_p (f1+f2))<=f2.(max_p f2) by AA10,A1;
f2.(max_p f2)=max f2 by AA30;
hence max (f1+f2)<=(max f1) +(max f2) by A10,A6,A7,A8,REAL_1:55;
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 A1: len f1=len f2 & len f1>0;then
A4: len (f1+f2)=len f1 by EUCLID_2:6;then
A11: min_p (f1+f2) in dom (f1+f2) by A1,AA20;then
A3: 1<=min_p (f1+f2) & min_p (f1+f2)<=len (f1+f2) by FINSEQ_3:27;
A10: min (f1+f2)=(f1+f2).(min_p (f1+f2)) by AA40
.=f1.(min_p (f1+f2)) + f2.(min_p (f1+f2)) by RVSUM_1:26,A11;
A5: min_p (f1+f2) in Seg len f1 by FINSEQ_1:3,A3,A4;then
min_p (f1+f2) in dom f1 by FINSEQ_1:def 3;then
A6: f1.(min_p (f1+f2))>=f1.(min_p f1) by AA20,A1;
A7: f1.(min_p f1)=min f1 by AA40;
min_p (f1+f2) in dom f2 by A5,A1,FINSEQ_1:def 3;then
A8: f2.(min_p (f1+f2))>=f2.(min_p f2) by AA20,A1;
f2.(min_p f2)=min f2 by AA40;
hence min (f1+f2)>=(min f1) +(min f2) by A10,A6,A7,A8,REAL_1:55;
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 A1: len f>0 & a>0;
A4: len (a*f)=len f by EUCLID_2:8;
A14: dom (a*f)=dom f by RVSUM_1:65;
A11: max_p (a*f) in dom (a*f) by A4,A1,AA10;then
A3: 1<=max_p (a*f) & max_p (a*f)<=len (a*f) by FINSEQ_3:27;
A10: max (a*f)=(a*f).(max_p (a*f)) by AA30
.=a*(f.(max_p (a*f))) by RVSUM_1:66;
max_p (a*f) in Seg len f by FINSEQ_1:3,A3,A4;then
A5b: max_p (a*f) in dom f by FINSEQ_1:def 3;then
A6: f.(max_p (a*f))<=f.(max_p f) by AA10,A1;
A20: a*(f.(max_p (f)))=(a*f).(max_p (f)) by RVSUM_1:66;
A21: a*(f.(max_p (a*f)))=(a*f).(max_p (a*f)) by RVSUM_1:66;
A15: max_p (f) in dom (a*f) by A1,AA10,A14;then
(a*f).(max_p (f))<=(a*f).(max_p (a*f)) by AA10,A1,A4;then
f.(max_p (f))<=f.(max_p (a*f)) by A1,A20,A21,REAL_1:70;then
A12: f.(max_p (f))=f.(max_p (a*f)) by A6,AXIOMS:21;
max_p (f) in dom (a*f) by A14,AA10,A1;then
A6b: (a*f).(max_p (a*f))>=(a*f).(max_p f) by AA10,A1,A4;
f.(max_p (f))>= f.(max_p (a*f)) by A5b,AA10,A1;then
A19: a*(f.(max_p (f)))>=a*(f.(max_p (a*f))) by A1,AXIOMS:25;
A17: (a*f).(max_p (a*f))=(a*f).(max_p f) by A6b,AXIOMS:21,A21,A19,A20;
A13: f.(max_p f)=max f by AA30;
A16: max_p (a*f)>=max_p f by AA10,A1,A12,A11,A14;
max_p (a*f)<=max_p f by A17,AA10,A1,A4,A15;
hence max (a*f)=a*(max f) & max_p (a*f)=max_p f
by A10,A13,A16,AXIOMS:21;
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 A1: len f>0 & a>0;
A4: len (a*f)=len f by EUCLID_2:8;
A14: dom (a*f)=dom f by RVSUM_1:65;
A11: min_p (a*f) in dom (a*f) by A4,A1,AA20;then
A3: 1<=min_p (a*f) & min_p (a*f)<=len (a*f) by FINSEQ_3:27;
A10: min (a*f)=(a*f).(min_p (a*f)) by AA40
.=a*(f.(min_p (a*f))) by RVSUM_1:66;
A5b: min_p (a*f) in dom f by A3,A4,FINSEQ_3:27;then
A6: f.(min_p (a*f))>=f.(min_p f) by AA20,A1;
A20: a*(f.(min_p (f)))=(a*f).(min_p (f)) by RVSUM_1:66;
A21: a*(f.(min_p (a*f)))=(a*f).(min_p (a*f)) by RVSUM_1:66;
A15: min_p (f) in dom (a*f) by A1,AA20,A14;then
(a*f).(min_p (f))>=(a*f).(min_p (a*f)) by AA20,A1,A4;then
f.(min_p (f))>=f.(min_p (a*f)) by A1,A20,A21,REAL_1:70;then
A12: f.(min_p (f))=f.(min_p (a*f)) by A6,AXIOMS:21;
min_p (f) in dom (a*f) by A14,AA20,A1;then
A6b: (a*f).(min_p (a*f))<=(a*f).(min_p f) by AA20,A1,A4;
f.(min_p (f))<= f.(min_p (a*f)) by A5b,AA20,A1;then
A19: a*(f.(min_p (f)))<=a*(f.(min_p (a*f))) by A1,AXIOMS:25;
A17: (a*f).(min_p (a*f))=(a*f).(min_p f) by A6b,AXIOMS:21,A21,A19,A20;
A13: f.(min_p f)=min f by AA40;
A16: min_p (a*f)>=min_p f by AA20,A1,A12,A11,A14;
min_p (a*f)<=min_p f by A17,AA20,A1,A4,A15;
hence min (a*f)=a*(min f) & min_p (a*f)=min_p f
by A10,A13,A16,AXIOMS:21;
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;
A4: len (-f)=len f by EUCLID_2:5;
A14: dom (-f)=dom f by RVSUM_1:34;
A11: max_p (-f) in dom (-f) by A4,A1,AA10;then
A3: 1<=max_p (-f) & max_p (-f)<=len (-f) by FINSEQ_3:27;
A10: max (-f)=(-f).(max_p (-f)) by AA30
.=-(f.(max_p (-f))) by RVSUM_1:35;
A15: min_p (f) in dom (-f) by A1,AA20,A14;
A20: -(f.(min_p (f)))=(-f).(min_p (f)) by RVSUM_1:35;
A21: -(f.(max_p (-f)))=(-f).(max_p (-f)) by RVSUM_1:35;
max_p (-f) in Seg len f by FINSEQ_1:3,A3,A4;then
A5b: max_p (-f) in dom f by FINSEQ_1:def 3;
(-f).(max_p (-f))>=(-f).(min_p f) by AA10,A1,A4,A15;then
A6: f.(max_p (-f))<=f.(min_p f) by A20,A21,REAL_1:50;
f.(min_p (f))<=f.(max_p (-f)) by A1,AA20,A5b;then
A12: f.(min_p (f))=f.(max_p (-f)) by A6,AXIOMS:21;
min_p (f) in dom (-f) by A14,AA20,A1;then
A6b: (-f).(max_p (-f))>=(-f).(min_p f) by AA10,A1,A4;
f.(min_p (f))<= f.(max_p (-f)) by A5b,AA20,A1;then
A19: -(f.(min_p (f)))>=-(f.(max_p (-f))) by REAL_1:50;
A17: (-f).(max_p (-f))=(-f).(min_p f) by A6b,AXIOMS:21,A21,A19,A20;
A13: f.(min_p f)=min f by AA40;
A16: max_p (-f)>=min_p f by AA20,A1,A12,A11,A14;
max_p (-f)<=min_p f by A17,AA10,A1,A4,A15;
hence max (-f)=-(min f) & max_p (-f)=min_p f by A10,A13,A16,AXIOMS:21;
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;
A4: len (-f)=len f by EUCLID_2:5;
A14: dom (-f)=dom f by RVSUM_1:34;
A11: min_p (-f) in dom (-f) by A4,A1,AA20;then
A3: 1<=min_p (-f) & min_p (-f)<=len (-f) by FINSEQ_3:27;
A10: min (-f)=(-f).(min_p (-f)) by AA40
.=-(f.(min_p (-f))) by RVSUM_1:35;
A15: max_p (f) in dom (-f) by A1,AA10,A14;
A20: -(f.(max_p (f)))=(-f).(max_p (f)) by RVSUM_1:35;
A21: -(f.(min_p (-f)))=(-f).(min_p (-f)) by RVSUM_1:35;
min_p (-f) in Seg len f by FINSEQ_1:3,A3,A4;then
A5b: min_p (-f) in dom f by FINSEQ_1:def 3;
(-f).(min_p (-f))<=(-f).(max_p f) by AA20,A1,A4,A15;then
A6: f.(min_p (-f))>=f.(max_p f) by A20,A21,REAL_1:50;
f.(max_p (f))>=f.(min_p (-f)) by A1,AA10,A5b;then
A12: f.(max_p (f))=f.(min_p (-f)) by A6,AXIOMS:21;
max_p (f) in dom (-f) by A14,AA10,A1;then
A6b: (-f).(min_p (-f))<=(-f).(max_p f) by AA20,A1,A4;
f.(max_p (f))>= f.(min_p (-f)) by A5b,AA10,A1;then
A19: -(f.(max_p (f)))<=-(f.(min_p (-f))) by REAL_1:50;
A17: (-f).(min_p (-f))=(-f).(max_p f) by A6b,AXIOMS:21,A21,A19,A20;
A13: f.(max_p f)=max f by AA30;
A16: min_p (-f)>=max_p f by AA10,A1,A12,A11,A14;
min_p (-f)<=max_p f by A17,AA20,A1,A4,A15;
hence min (-f)=-(max f) & min_p (-f)=max_p f by A10,A13,A16,AXIOMS:21;
end;
theorem for f being FinSequence of REAL,n being Nat st
1<=n & n<len f
holds max (f/^n)<= max f & min (f/^n)>= min f
proof let f be FinSequence of REAL,n be Nat;
assume A1: 1<=n & n<len f;
A2: 0<len f by A1,NAT_1:18;
B1: len (f/^n)=len f -n by A1,RFINSEQ:def 2;then
B12: len (f/^n)>0 by A1,SQUARE_1:11;then
B6: (max_p (f/^n)) in dom (f/^n) by AA10;then
B2: 1<= (max_p (f/^n)) & (max_p (f/^n))<=len (f/^n) by FINSEQ_3:27;
(max_p (f/^n))+n<=len f-n+n by B1,B2,REAL_1:55;then
B4: (max_p (f/^n))+n<=len f by XCMPLX_1:27;
B5: 1+n<=(max_p (f/^n))+n by B2,REAL_1:55;
1<=1+n by NAT_1:37;then
1<= ((max_p (f/^n))+n) & ((max_p (f/^n))+n)<=len f
by B4,B5,AXIOMS:22;then
B3: ((max_p (f/^n))+n) in dom f by FINSEQ_3:27;
f.( (max_p (f/^n))+n)=(f/^n).(max_p (f/^n)) by A1,B6,RFINSEQ:def 2
.=max (f/^n) by AA30;then
max (f/^n)<= f.(max_p f) by B3,AA10,A2;then
B10: max (f/^n)<= max f by AA30;
B6: (min_p (f/^n)) in dom (f/^n) by B12,AA20;then
B2: 1<= (min_p (f/^n)) & (min_p (f/^n))<=len (f/^n) by FINSEQ_3:27;
(min_p (f/^n))+n<=len f-n+n by B1,B2,REAL_1:55;then
B4: (min_p (f/^n))+n<=len f by XCMPLX_1:27;
B5: 1+n<=(min_p (f/^n))+n by B2,REAL_1:55;
1<=1+n by NAT_1:37;then
1<= ((min_p (f/^n))+n) & ((min_p (f/^n))+n)<=len f
by B4,B5,AXIOMS:22;then
B3: ((min_p (f/^n))+n) in dom f by FINSEQ_3:27;
f.( (min_p (f/^n))+n)=(f/^n).(min_p (f/^n)) by A1,B6,RFINSEQ:def 2
.=min (f/^n) by AA40;then
min (f/^n)>= f.(min_p f) by B3,AA20,A2;
hence max (f/^n)<= max f & min (f/^n)>= min f by B10,AA40;
end;
BB132P: 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:17;
A3: len f=len g & dom f=dom g by A1,RFINSEQ:16;
per cases;
suppose B0: len f>0;then
B1: max_p f in dom (g*P) by AA10,A2;then
B4: (g*P).(max_p f)=g.(P.(max_p f)) by FUNCT_1:22;
B2: max_p f in dom g by B1,A2,A3;
B3: dom g=Seg len g by FINSEQ_1:def 3;
B10: 0+1<=len f by B0,NAT_1:38;
A3d: rng P=dom g by FUNCT_2:def 3;
dom g=Seg len g by FINSEQ_1:def 3;then
dom g <>{} by B10,A3,FINSEQ_1:3;then
dom P=dom g by FUNCT_2:def 1;then
A20: P.(max_p f) in rng P by B2,FUNCT_1:def 5;then
reconsider n=P.(max_p f) as Nat by A3d;
1<=n & n<=len g by FINSEQ_1:3,B3,A3d,A20;then
g.n <= max g by BB10;
hence max f<=max g by B4,A2,AA30;
suppose B0: len f<=0;
B1: len f=0 by B0,NAT_1:18;then
f={} by FINSEQ_1:25;
hence max f<=max g by A3,B1,FINSEQ_1:25;
end;
theorem BB132: 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
A2: max f <= max g by BB132P;
max g <= max f by BB132P,A1;
hence max f=max g by A2,AXIOMS:21;
end;
BB134P: 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:17;
A3: len f=len g & dom f=dom g by A1,RFINSEQ:16;
per cases;
suppose B0: len f>0;then
B1: min_p f in dom (g*P) by AA20,A2;then
B4: (g*P).(min_p f)=g.(P.(min_p f)) by FUNCT_1:22;
B2: min_p f in dom g by B1,A2,A1,RFINSEQ:16;
B3: dom g=Seg len g by FINSEQ_1:def 3;
B10: 0+1<=len f by B0,NAT_1:38;
A3d: rng P=dom g by FUNCT_2:def 3;
dom g=Seg len g by FINSEQ_1:def 3;then
1 in dom g by B10,A3,FINSEQ_1:3;then
dom g <>{} by XBOOLE_0:def 1;then
dom P=dom g by FUNCT_2:def 1;then
A20: P.(min_p f) in rng P by B2,FUNCT_1:def 5;then
reconsider n=P.(min_p f) as Nat by A3d;
1<=n & n<=len g by FINSEQ_1:3,B3,A3d,A20;then
g.n >= min g by BB20;
hence min f>=min g by B4,A2,AA40;
suppose B0: len f<=0;
B1: len f=0 by B0,NAT_1:18;then
f={} by FINSEQ_1:25;
hence min f>=min g by A3,B1,FINSEQ_1:25;
end;
theorem BB134: 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
A2: min f >= min g by BB134P;
min g >= min f by BB134P,A1;
hence min f=min g by A2,AXIOMS:21;
end;
definition let f be FinSequence of REAL;
func sort_d f -> non-increasing FinSequence of REAL means
::Descend Sorting or Rearrangement of FinSequences
:AA50: f,it are_fiberwise_equipotent;
existence by RFINSEQ:35;
uniqueness
proof
thus for f1,f2 being non-increasing FinSequence of REAL st
f,f1 are_fiberwise_equipotent & f,f2 are_fiberwise_equipotent
holds f1=f2
proof let f1,f2 be non-increasing FinSequence of REAL;
assume f,f1 are_fiberwise_equipotent & f,f2 are_fiberwise_equipotent;
then f1,f2 are_fiberwise_equipotent by RFINSEQ:2;
hence f1=f2 by RFINSEQ:36;
end;
end;
end;
Lm4:
for D be non empty set, f be FinSequence of D st len f<=n holds f|n = f
by TOPREAL1:2;
theorem Th31:
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 by FINSEQ_1:32;
then for n st n in dom R & n+1 in dom R holds R.n<=R.(n+1) by FINSEQ_1:26;
hence thesis by INTEGRA2:def 1;
suppose len R = 1;
then A2: dom R = {1} by FINSEQ_1:4,def 3;
now let n; assume n in dom R & n+1 in dom R;
then n = 1 & n+1 = 1 by A2,TARSKI:def 1;
hence R.n<=R.(n+1);
end;
hence thesis by INTEGRA2:def 1;
end;
theorem Th32:
for R be FinSequence of REAL holds
R is non-decreasing
iff
for n,m be Nat st n in dom R & m in dom R & n<m holds R.n<=R.m
proof let R be FinSequence of REAL;
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 assume
A1: R is non-decreasing;
defpred P[Nat] means $1 in dom R implies
for n st n in dom R & n<$1 holds R.n<=R.$1;
Seg len R = dom R by FINSEQ_1:def 3;
then A2: P[0] by FINSEQ_1:3;
A3: for m st P[m] holds P[m+1]
proof let m; assume
A4: P[m]; assume
A5: m+1 in dom R;
let n; assume
A6: n in dom R & n<m+1;
then A7: 1<=m+1 & m+1<=len R & 1<=n & n<=len R & n<=m & m<=m+1
by A5,FINSEQ_3:27,NAT_1:38;
then A8: 1<=m & m<=len R by AXIOMS:22;
then A9: m in dom R by FINSEQ_3:27;
set t = R.m, r = R.n, s = R.(m+1);
now per cases;
case n = m; hence r<=s by A1,A5,A6,INTEGRA2:def 1;
case n <> m;
then n<m by A7,REAL_1:def 5;
then A10: r<=t by A4,A6,A8,FINSEQ_3:27;
t<=s by A1,A5,A9,INTEGRA2:def 1;
hence r<=s by A10,AXIOMS:22;
end;
hence r<=s;
end;
for m holds P[m] from Ind(A2,A3);
hence thesis;
end; assume
A11: for n,m st n in dom R & m in dom R & n<m holds R.n<=R.m;
let n; assume
A12: n in dom R & n+1 in dom R;
n<n+1 by NAT_1:38;
hence thesis by A11,A12;
end;
Lm5:
for f,g be non-decreasing FinSequence of REAL, 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 FinSequence of REAL, n; assume
A1: len f = n+1 & len f = len g & f,g are_fiberwise_equipotent;
0<n+1 by NAT_1:19;
then 0+1<=n+1 by NAT_1:38;
then A2: n+1 in dom f & n+1 in dom g by A1,FINSEQ_3:27;
set r = f.(n+1), s = g.(n+1);
A3: now assume A4: r <> s;
A5: rng f = rng g by A1,RFINSEQ:1;
now per cases by A4,REAL_1:def 5;
case A6: r<s;
s in rng f by A2,A5,FUNCT_1:def 5;
then consider m such that
A7: m in dom f & f.m = s by FINSEQ_2:11;
A8: 1<=m & m<=len f by A7,FINSEQ_3:27;
now per cases;
case m = len f;
hence contradiction by A1,A6,A7;
case m <> len f;
then m<n+1 by A1,A8,REAL_1:def 5;
hence contradiction by A2,A6,A7,Th32;
end;
hence contradiction;
case A9: r>s;
r in rng g by A2,A5,FUNCT_1:def 5;
then consider m such that
A10: m in dom g & g.m = r by FINSEQ_2:11;
A11: 1<=m & m<=len g by A10,FINSEQ_3:27;
now per cases;
case m = len g;
hence contradiction by A1,A9,A10;
case m <> len g;
then m<n+1 by A1,A11,REAL_1:def 5;
hence contradiction by A2,A9,A10,Th32;
end;
hence contradiction;
end;
hence contradiction;
end;
hence f.(len f) = g.(len g) by A1;
A12: f = (f|n)^<*r*> & g = (g|n)^<*r*> by A1,A3,RFINSEQ:20;
now let x be set;
card((f|n)"{x}) + card(<*r*>"{x}) = card (f"{x}) by A12,FINSEQ_3:63
.= card(g"{x}) by A1,RFINSEQ:def 1
.= card((g|n)"{x}) + card(<*r*>"{x}) by A12,FINSEQ_3:63;
hence card((f|n)"{x}) = card((g|n)"{x}) by XCMPLX_1:2;
end;
hence thesis by RFINSEQ:def 1;
end;
theorem Th33:
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 A1: n = 0; then n<=len f by NAT_1:18;
then len fn = 0 by A1,TOPREAL1:3;
hence thesis by Th31;
case n <> 0;
then 0<n by NAT_1:19;
then A2: 0+1<=n by NAT_1:38;
now per cases;
case len f<=n; hence thesis by Lm4;
case n<len f;
then A3: n in dom f & len fn = n by A2,FINSEQ_3:27,TOPREAL1:3;
now let m; assume
A4: m in dom fn & m+1 in dom fn;
dom f = Seg len f & dom fn = Seg len fn by FINSEQ_1:def 3;
then f.m = fn.m & f.(m+1) = fn.(m+1) & m in dom f & m+1 in dom f
by A3,A4,RFINSEQ:19;
hence fn.m<=fn.(m+1) by INTEGRA2:def 1;
end;
hence thesis by INTEGRA2:def 1;
end;
hence thesis;
end;
hence thesis;
end;
Lm8:
for n holds for g1,g2 be non-decreasing FinSequence of REAL st
n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2
proof
defpred P[Nat] means
for g1,g2 be non-decreasing FinSequence of REAL st $1 = len g1 &
g1,g2 are_fiberwise_equipotent holds g1 = g2;
A1: P[0]
proof
let g1,g2 be non-decreasing FinSequence of REAL; assume that
A2: len g1 = 0 and
A3: g1,g2 are_fiberwise_equipotent;
len g2 = len g1 by A3,RFINSEQ:16;
then g1 = <*>REAL & g2 = <*>REAL by A2,FINSEQ_1:32;
hence thesis;
end;
A4: for n st P[n] holds P[n+1]
proof let n; assume
A5: P[n];
let g1,g2 be non-decreasing FinSequence of REAL; assume that
A6: len g1 = n+1 and
A7: g1,g2 are_fiberwise_equipotent;
A8: len g2 = len g1 by A7,RFINSEQ:16;
then A9: g1.(len g1) = g2.(len g2) & g1|n, g2|n are_fiberwise_equipotent
by A6,A7,Lm5;
n<=len g1 by A6,NAT_1:29;
then A10: len(g1|n) = n & len(g2|n) = n by A8,TOPREAL1:3;
reconsider g1n = g1|n, g2n = g2|n as non-decreasing FinSequence of REAL
by Th33;
set r = g1.(n+1);
A11: g1n = g2n by A5,A9,A10;
(g1|n)^<*r*> = g1 & (g2|n)^<*r*> = g2 by A6,A8,A9,RFINSEQ:20;
hence thesis by A11;
end;
for m holds P[m] from Ind(A1,A4);
hence thesis;
end;
theorem Th36:
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; assume
A1: g1,g2 are_fiberwise_equipotent;
len g1 = len g1;
hence thesis by A1,Lm8;
end;
definition let f be FinSequence of REAL;
func sort_a f -> non-decreasing FinSequence of REAL means
::Ascend Sorting or Rearrangement of FinSequences
:AA60: f,it are_fiberwise_equipotent;
existence by INTEGRA2:3;
uniqueness
proof
thus for f1,f2 being non-decreasing FinSequence of REAL st
f,f1 are_fiberwise_equipotent & f,f2 are_fiberwise_equipotent
holds f1=f2
proof let f1,f2 be non-decreasing FinSequence of REAL;
assume f,f1 are_fiberwise_equipotent & f,f2 are_fiberwise_equipotent;
then f1,f2 are_fiberwise_equipotent by RFINSEQ:2;
hence f1=f2 by Th36;
end;
end;
end;
theorem for f being non-increasing FinSequence of REAL
holds sort_d f=f by AA50;
theorem for f being non-decreasing FinSequence of REAL
holds sort_a f=f by AA60;
theorem for f being FinSequence of REAL
holds sort_d (sort_d f)=sort_d f by AA50;
theorem for f being FinSequence of REAL
holds sort_a (sort_a f)=sort_a f by AA60;
theorem BB170: for f being FinSequence of REAL st f is non-increasing
holds -f is non-decreasing
proof let f be FinSequence of REAL;
assume f is non-increasing;then
A2: for n being Nat st n in dom f & n+1 in dom f holds f.n >= f.(n+1)
by RFINSEQ:def 4;
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;
assume B1: n in dom (-f) & n+1 in dom (-f);
dom (-f)=dom f by RVSUM_1:34;then
B2: f.n >= f.(n+1) by A2,B1;
B3: (-f).n=-(f.n) by RVSUM_1:35;
(-f).(n+1)= -(f.(n+1)) by RVSUM_1:35;
hence (-f).n <= (-f).(n+1) by B2,B3,REAL_1:50;
end;
hence -f is non-decreasing by INTEGRA2:def 1;
end;
theorem BB180: for f being FinSequence of REAL st f is non-decreasing
holds -f is non-increasing
proof let f be FinSequence of REAL;
assume f is non-decreasing;then
A2: for n being Nat st n in dom f & n+1 in dom f holds f.n <= f.(n+1)
by INTEGRA2:def 1;
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;
assume B1: n in dom (-f) & n+1 in dom (-f);
dom (-f)=dom f by RVSUM_1:34;then
B2: f.n <= f.(n+1) by A2,B1;
B3: (-f).n=-(f.n) by RVSUM_1:35;
(-f).(n+1)= -(f.(n+1)) by RVSUM_1:35;
hence (-f).n >= (-f).(n+1) by B2,B3,REAL_1:50;
end;
hence -f is non-increasing by RFINSEQ:def 4;
end;
theorem BB185: 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 A1: f = g*P & len g>=1;
A3: rng P=dom g by FUNCT_2:def 3;
A3b: dom g=Seg len g by FINSEQ_1:def 3;then
1 in dom g by A1,FINSEQ_1:3;then
dom g <>{} by XBOOLE_0:def 1;then
A7: dom P=dom g by FUNCT_2:def 1;
A2b: dom (-g)=dom g by RVSUM_1:34;
A4: dom (-f)=dom (g*P) by A1,RVSUM_1:34;then
A6: dom (-f)=dom P by A3,RELAT_1:46;then
A5: dom (-f)=dom ((-g)*P) by A2b,A3,RELAT_1:46;
A8: rng ((-g)*P) = rng (-g) by RELAT_1:47,A3,A2b;
A9: rng (-g) c= REAL by FINSEQ_1:def 4;
(-g)*P is FinSequence by A5,A6,A7,A3b,FINSEQ_1:def 2;then
reconsider k=(-g)*P as FinSequence of REAL by A8,A9,FINSEQ_1:def 4;
for i being Nat st i in dom (-f) holds (-f).i=k.i
proof let i be Nat;
assume B1: i in dom (-f);then
P.i in rng P by A6,FUNCT_1:12;then
reconsider j=P.i as Nat by A3;
(-f).i=-(f.i) by RVSUM_1:35
.=-(g.(P.i)) by A1,A4,B1,FUNCT_1:22
.=(-g).(j) by RVSUM_1:35 .=((-g)*P).i by A5,B1,FUNCT_1:22;
hence (-f).i=k.i;
end;
hence -f=(-g)*P by A5,FINSEQ_1:17;
end;
theorem BB187: 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:17;
A3: dom (-g)=dom g by RVSUM_1:34;
now per cases;
case len g>=1;
hence -f=(-g)*P by A2,BB185;
case len g<1;then len g<0+1;then
B1: len g<=0 by NAT_1:38;
B2: len g=0 by B1,NAT_1:18;then
B3: len f=0 by A1,RFINSEQ:16;then
B5: f={} by FINSEQ_1:25;
B6: g={} by FINSEQ_1:25,B2;
len (-f)=0 by EUCLID_2:5,B3;then
-f ={} by FINSEQ_1:25;
hence -f=(-g)*P by B5,B6,A2;
end;
hence -f,-g are_fiberwise_equipotent by RFINSEQ:17,A3;
end;
theorem for f being FinSequence of REAL holds
sort_d (-f) = - (sort_a f)
proof let f be FinSequence of REAL;
A3: f,sort_a(f) are_fiberwise_equipotent by AA60;
A2: -sort_d (-f) is non-decreasing by BB170;
-f,sort_d(-f) are_fiberwise_equipotent by AA50;then
--f,-sort_d(-f) are_fiberwise_equipotent by BB187;then
sort_a(f),-sort_d (-f) are_fiberwise_equipotent by A3,RFINSEQ:2;then
-sort_d (-f)=sort_a f by Th36,A2;
hence sort_d (-f)=- (sort_a f);
end;
theorem for f being FinSequence of REAL holds
sort_a (-f) = - (sort_d f)
proof let f be FinSequence of REAL;
A3: f,sort_d(f) are_fiberwise_equipotent by AA50;
A2: -sort_a (-f) is non-increasing by BB180;
-f,sort_a(-f) are_fiberwise_equipotent by AA60;then
--f,-sort_a(-f) are_fiberwise_equipotent by BB187;then
sort_d(f),-sort_a (-f) are_fiberwise_equipotent by A3,RFINSEQ:2;then
-sort_a (-f)=sort_d f by RFINSEQ:36,A2;
hence sort_a (-f)=- (sort_d f);
end;
theorem BB202: 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 AA50;
hence dom (sort_d f)=dom f & len (sort_d f)=len f by RFINSEQ:16;
end;
theorem BB204: 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 AA60;
hence dom (sort_a f)=dom f & len (sort_a f)=len f by RFINSEQ:16;
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;then
A2: len f>0 by AXIOMS:22;
A7: len (sort_d f)=len f by BB202;then
1 in Seg len (sort_d f) by A1,FINSEQ_1:3;then
A3: 1 in dom (sort_d f) by FINSEQ_1:def 3;
A5: 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 B1: i in dom (sort_d f) & r1=(sort_d f).i & r2=(sort_d f).1;
i in Seg len (sort_d f) by B1,FINSEQ_1:def 3;then
B3: 1<=i by FINSEQ_1:3;
now per cases;
case 1=i;
hence r1<=r2 by B1;
case 1<>i;then 1<i by B3,REAL_1:def 5;
hence r1<=r2 by B1,A3,RFINSEQ:32;
end;
hence r1<=r2;
end;
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 j in dom (sort_d f) & (sort_d f).j=(sort_d f).1;then
j in Seg len (sort_d f) by FINSEQ_1:def 3;
hence 1<=j by FINSEQ_1:3;
end;then
A14: max_p(sort_d f)=1 by AA10,A7,A3,A2,A5;
A14b: f,(sort_d f) are_fiberwise_equipotent by AA50;
A15: (sort_d f).1=max (sort_d f) by A14,AA30.=max f by BB132,A14b;
A7: len (sort_a f)=len f by BB204;then
A3: 1 in dom (sort_a f) by A1,FINSEQ_3:27;
A5: for i being Nat,r1,r2 being Real st
i in dom (sort_a f) & r1=(sort_a f).i & r2=(sort_a f).1
holds r1>=r2
proof let i be Nat,r1,r2 be Real;
assume B1: i in dom (sort_a f) & r1=(sort_a f).i & r2=(sort_a f).1;then
B3: 1<=i by FINSEQ_3:27;
per cases;
suppose 1=i;
hence r1>=r2 by B1;
suppose 1<>i;then 1<i by B3,REAL_1:def 5;
hence r1>=r2 by B1,A3,Th32;
end;
a: 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:27; then
A19: min_p(sort_a f)=1 by AA20,A7,A3,A2,A5;
A14b: f,(sort_a f) are_fiberwise_equipotent by AA60;
(sort_a f).1=min (sort_a f) by A19,AA40.=min f by BB134,A14b;
hence thesis by A14,A15,a,AA20,A7,A3,A2,A5;
end;