:: RFINSEQ2 semantic presentation
begin
definition
let f be FinSequence of REAL ;
func max_p f -> Element of NAT means :Def1: :: RFINSEQ2:def 1
( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . it holds
it <= j ) ) ) );
existence
ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof
A1: dom f = Seg (len f) by FINSEQ_1:def_3;
percases ( len f = 0 or len f <> 0 ) ;
suppose len f = 0 ; ::_thesis: ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
hence ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) ; ::_thesis: verum
end;
supposeA2: len f <> 0 ; ::_thesis: ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
defpred S1[ Element of NAT ] means ex n being Element of NAT st
( ( $1 <> 0 implies ( n <= $1 & n in dom f ) ) & ( for i being Element of NAT
for r1, r2 being Real st i <= $1 & i in dom f & r1 = f . i & r2 = f . n holds
r1 <= r2 ) & ( for j being Element of NAT st j <= $1 & j in dom f & f . j = f . n holds
n <= j ) );
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then consider n1 being Element of NAT such that
A4: ( k <> 0 implies ( n1 <= k & n1 in dom f ) ) and
A5: for i being Element of NAT
for 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 Element of NAT st j <= k & j in dom f & f . j = f . n1 holds
n1 <= j ;
percases ( k = 0 or k <> 0 ) ;
supposeA7: k = 0 ; ::_thesis: S1[k + 1]
A8: dom f = Seg (len f) by FINSEQ_1:def_3;
A9: for i being Element of NAT
for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 <= r2
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 <= r2
let r1, r2 be Real; ::_thesis: ( i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 implies r1 <= r2 )
assume that
A10: i <= 1 and
A11: i in dom f and
A12: ( r1 = f . i & r2 = f . 1 ) ; ::_thesis: r1 <= r2
1 <= i by A11, FINSEQ_3:25;
hence r1 <= r2 by A10, A12, XXREAL_0:1; ::_thesis: verum
end;
len f >= 0 + 1 by A2, NAT_1:13;
then A13: 1 in dom f by A8, FINSEQ_1:1;
for j being Element of NAT st j <= 1 & j in dom f & f . j = f . 1 holds
1 <= j by A8, FINSEQ_1:1;
hence S1[k + 1] by A7, A13, A9; ::_thesis: verum
end;
supposeA14: k <> 0 ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_f_._n1_>=_f_._(k_+_1)_&_S1[k_+_1]_)_or_(_f_._n1_<_f_._(k_+_1)_&_S1[k_+_1]_)_)
percases ( f . n1 >= f . (k + 1) or f . n1 < f . (k + 1) ) ;
caseA15: f . n1 >= f . (k + 1) ; ::_thesis: S1[k + 1]
A16: for i being Element of NAT
for 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 Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 <= r2
let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 <= r2 )
assume that
A17: i <= k + 1 and
A18: i in dom f and
A19: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 <= r2
percases ( i < k + 1 or i >= k + 1 ) ;
suppose i < k + 1 ; ::_thesis: r1 <= r2
then i <= k by NAT_1:13;
hence r1 <= r2 by A5, A18, A19; ::_thesis: verum
end;
suppose i >= k + 1 ; ::_thesis: r1 <= r2
hence r1 <= r2 by A15, A17, A19, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
A20: n1 <= k + 1 by A4, A14, NAT_1:13;
A21: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j )
assume that
A22: j <= k + 1 and
A23: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j
now__::_thesis:_(_(_j_<_k_+_1_&_n1_<=_j_)_or_(_j_>=_k_+_1_&_n1_<=_j_)_)
percases ( j < k + 1 or j >= k + 1 ) ;
case j < k + 1 ; ::_thesis: n1 <= j
then j <= k by NAT_1:13;
hence n1 <= j by A6, A23; ::_thesis: verum
end;
case j >= k + 1 ; ::_thesis: n1 <= j
hence n1 <= j by A20, A22, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence n1 <= j ; ::_thesis: verum
end;
( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, NAT_1:13;
hence S1[k + 1] by A16, A21; ::_thesis: verum
end;
caseA24: f . n1 < f . (k + 1) ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_k_+_1_>_len_f_&_S1[k_+_1]_)_or_(_k_+_1_<=_len_f_&_S1[k_+_1]_)_)
percases ( k + 1 > len f or k + 1 <= len f ) ;
caseA25: k + 1 > len f ; ::_thesis: S1[k + 1]
A26: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j )
assume that
j <= k + 1 and
A27: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j
percases ( j < k + 1 or j >= k + 1 ) ;
suppose j < k + 1 ; ::_thesis: n1 <= j
then j <= k by NAT_1:13;
hence n1 <= j by A6, A27; ::_thesis: verum
end;
suppose j >= k + 1 ; ::_thesis: n1 <= j
then k < j by NAT_1:13;
hence n1 <= j by A4, A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A28: k >= len f by A25, NAT_1:13;
A29: for i being Element of NAT
for 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 Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 <= r2
let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 <= r2 )
assume that
i <= k + 1 and
A30: i in dom f and
A31: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 <= r2
i <= len f by A1, A30, FINSEQ_1:1;
then i <= k by A28, XXREAL_0:2;
hence r1 <= r2 by A5, A30, A31; ::_thesis: verum
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 S1[k + 1] by A29, A26; ::_thesis: verum
end;
caseA32: k + 1 <= len f ; ::_thesis: S1[k + 1]
set n2 = k + 1;
A33: for i being Element of NAT
for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds
r1 <= r2
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds
r1 <= r2
let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) implies r1 <= r2 )
assume that
A34: i <= k + 1 and
A35: i in dom f and
A36: r1 = f . i and
A37: r2 = f . (k + 1) ; ::_thesis: r1 <= r2
percases ( i < k + 1 or i >= k + 1 ) ;
supposeA38: i < k + 1 ; ::_thesis: r1 <= r2
reconsider r3 = f . n1 as Real ;
i <= k by A38, NAT_1:13;
then r1 <= r3 by A5, A35, A36;
hence r1 <= r2 by A24, A37, XXREAL_0:2; ::_thesis: verum
end;
suppose i >= k + 1 ; ::_thesis: r1 <= r2
hence r1 <= r2 by A34, A36, A37, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
A39: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . (k + 1) holds
k + 1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . (k + 1) implies k + 1 <= j )
assume that
j <= k + 1 and
A40: ( j in dom f & f . j = f . (k + 1) ) ; ::_thesis: k + 1 <= j
percases ( j < k + 1 or j >= k + 1 ) ;
suppose j < k + 1 ; ::_thesis: k + 1 <= j
then j <= k by NAT_1:13;
hence k + 1 <= j by A5, A24, A40; ::_thesis: verum
end;
suppose j >= k + 1 ; ::_thesis: k + 1 <= j
hence k + 1 <= j ; ::_thesis: verum
end;
end;
end;
1 <= 1 + k by NAT_1:12;
then ( k + 1 <> 0 implies ( k + 1 <= k + 1 & k + 1 in dom f ) ) by A1, A32, FINSEQ_1:1;
hence S1[k + 1] by A33, A39; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
end;
end;
( ( for i being Element of NAT
for r1, r2 being Real st i <= 0 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 <= r2 ) & ( for j being Element of NAT st j <= 0 & j in dom f & f . j = f . 1 holds
1 <= j ) ) by A1, FINSEQ_1:1;
then A41: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A41, A3);
then consider n1 being Element of NAT such that
A42: ( len f <> 0 implies ( n1 <= len f & n1 in dom f ) ) and
A43: for i being Element of NAT
for 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 Element of NAT st j <= len f & j in dom f & f . j = f . n1 holds
n1 <= j ;
A45: for j being Element of NAT st j in dom f & f . j = f . n1 holds
n1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j in dom f & f . j = f . n1 implies n1 <= j )
assume that
A46: j in dom f and
A47: f . j = f . n1 ; ::_thesis: n1 <= j
j <= len f by A46, FINSEQ_3:25;
hence n1 <= j by A44, A46, A47; ::_thesis: verum
end;
for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds
r1 <= r2
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds
r1 <= r2
let r1, r2 be Real; ::_thesis: ( i in dom f & r1 = f . i & r2 = f . n1 implies r1 <= r2 )
assume that
A48: i in dom f and
A49: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 <= r2
i <= len f by A48, FINSEQ_3:25;
hence r1 <= r2 by A43, A48, A49; ::_thesis: verum
end;
hence ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) by A2, A42, A45; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Element of NAT st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof
thus for m1, m2 being Element of NAT st ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 <= r2 ) & ( for j being Element of 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 Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) holds
m1 = m2 ::_thesis: verum
proof
let m1, m2 be Element of NAT ; ::_thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 <= r2 ) & ( for j being Element of 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 Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) implies m1 = m2 )
assume A50: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 <= r2 ) & ( for j being Element of 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 Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) ) ; ::_thesis: m1 = m2
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 m1 = m2 by XXREAL_0:1; ::_thesis: verum
end;
end;
end;
:: deftheorem Def1 defines max_p RFINSEQ2:def_1_:_
for f being FinSequence of REAL
for b2 being Element of NAT holds
( b2 = max_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );
definition
let f be FinSequence of REAL ;
func min_p f -> Element of NAT means :Def2: :: RFINSEQ2:def 2
( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . it holds
it <= j ) ) ) );
existence
ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof
A1: dom f = Seg (len f) by FINSEQ_1:def_3;
now__::_thesis:_(_(_len_f_=_0_&_ex_b1_being_Element_of_NAT_st_
(_(_len_f_=_0_implies_b1_=_0_)_&_(_len_f_>_0_implies_(_b1_in_dom_f_&_(_for_i_being_Element_of_NAT_
for_r1,_r2_being_Real_st_i_in_dom_f_&_r1_=_f_._i_&_r2_=_f_._b1_holds_
r1_>=_r2_)_&_(_for_j_being_Element_of_NAT_st_j_in_dom_f_&_f_._j_=_f_._b1_holds_
b1_<=_j_)_)_)_)_)_or_(_len_f_<>_0_&_ex_b1_being_Element_of_NAT_st_
(_(_len_f_=_0_implies_b1_=_0_)_&_(_len_f_>_0_implies_(_b1_in_dom_f_&_(_for_i_being_Element_of_NAT_
for_r1,_r2_being_Real_st_i_in_dom_f_&_r1_=_f_._i_&_r2_=_f_._b1_holds_
r1_>=_r2_)_&_(_for_j_being_Element_of_NAT_st_j_in_dom_f_&_f_._j_=_f_._b1_holds_
b1_<=_j_)_)_)_)_)_)
percases ( len f = 0 or len f <> 0 ) ;
case len f = 0 ; ::_thesis: ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
hence ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) ; ::_thesis: verum
end;
caseA2: len f <> 0 ; ::_thesis: ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
defpred S1[ Element of NAT ] means ex n being Element of NAT st
( ( $1 <> 0 implies ( n <= $1 & n in dom f ) ) & ( for i being Element of NAT
for r1, r2 being Real st i <= $1 & i in dom f & r1 = f . i & r2 = f . n holds
r1 >= r2 ) & ( for j being Element of NAT st j <= $1 & j in dom f & f . j = f . n holds
n <= j ) );
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then consider n1 being Element of NAT such that
A4: ( k <> 0 implies ( n1 <= k & n1 in dom f ) ) and
A5: for i being Element of NAT
for 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 Element of NAT st j <= k & j in dom f & f . j = f . n1 holds
n1 <= j ;
now__::_thesis:_(_(_k_=_0_&_S1[k_+_1]_)_or_(_k_<>_0_&_S1[k_+_1]_)_)
percases ( k = 0 or k <> 0 ) ;
caseA7: k = 0 ; ::_thesis: S1[k + 1]
A8: dom f = Seg (len f) by FINSEQ_1:def_3;
A9: for i being Element of NAT
for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 >= r2
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 >= r2
let r1, r2 be Real; ::_thesis: ( i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 implies r1 >= r2 )
assume that
A10: i <= 1 and
A11: i in dom f and
A12: ( r1 = f . i & r2 = f . 1 ) ; ::_thesis: r1 >= r2
1 <= i by A11, FINSEQ_3:25;
hence r1 >= r2 by A10, A12, XXREAL_0:1; ::_thesis: verum
end;
len f >= 0 + 1 by A2, NAT_1:13;
then A13: 1 in dom f by A8, FINSEQ_1:1;
for j being Element of NAT st j <= 1 & j in dom f & f . j = f . 1 holds
1 <= j by A8, FINSEQ_1:1;
hence S1[k + 1] by A7, A13, A9; ::_thesis: verum
end;
caseA14: k <> 0 ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_f_._n1_<=_f_._(k_+_1)_&_S1[k_+_1]_)_or_(_f_._n1_>_f_._(k_+_1)_&_S1[k_+_1]_)_)
percases ( f . n1 <= f . (k + 1) or f . n1 > f . (k + 1) ) ;
caseA15: f . n1 <= f . (k + 1) ; ::_thesis: S1[k + 1]
A16: for i being Element of NAT
for 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 Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 )
assume that
A17: i <= k + 1 and
A18: i in dom f and
A19: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 >= r2
percases ( i < k + 1 or i >= k + 1 ) ;
suppose i < k + 1 ; ::_thesis: r1 >= r2
then i <= k by NAT_1:13;
hence r1 >= r2 by A5, A18, A19; ::_thesis: verum
end;
suppose i >= k + 1 ; ::_thesis: r1 >= r2
hence r1 >= r2 by A15, A17, A19, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
A20: n1 <= k + 1 by A4, A14, NAT_1:13;
A21: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j )
assume that
A22: j <= k + 1 and
A23: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j
percases ( j < k + 1 or j >= k + 1 ) ;
suppose j < k + 1 ; ::_thesis: n1 <= j
then j <= k by NAT_1:13;
hence n1 <= j by A6, A23; ::_thesis: verum
end;
suppose j >= k + 1 ; ::_thesis: n1 <= j
hence n1 <= j by A20, A22, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, NAT_1:13;
hence S1[k + 1] by A16, A21; ::_thesis: verum
end;
caseA24: f . n1 > f . (k + 1) ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_k_+_1_>_len_f_&_S1[k_+_1]_)_or_(_k_+_1_<=_len_f_&_S1[k_+_1]_)_)
percases ( k + 1 > len f or k + 1 <= len f ) ;
caseA25: k + 1 > len f ; ::_thesis: S1[k + 1]
A26: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j )
assume that
j <= k + 1 and
A27: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j
percases ( j < k + 1 or j >= k + 1 ) ;
suppose j < k + 1 ; ::_thesis: n1 <= j
then j <= k by NAT_1:13;
hence n1 <= j by A6, A27; ::_thesis: verum
end;
suppose j >= k + 1 ; ::_thesis: n1 <= j
then k < j by NAT_1:13;
hence n1 <= j by A4, A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A28: k >= len f by A25, NAT_1:13;
A29: for i being Element of NAT
for 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 Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 )
assume that
i <= k + 1 and
A30: i in dom f and
A31: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 >= r2
i <= len f by A1, A30, FINSEQ_1:1;
then i <= k by A28, XXREAL_0:2;
hence r1 >= r2 by A5, A30, A31; ::_thesis: verum
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 S1[k + 1] by A29, A26; ::_thesis: verum
end;
caseA32: k + 1 <= len f ; ::_thesis: S1[k + 1]
set n2 = k + 1;
A33: for i being Element of NAT
for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds
r1 >= r2
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds
r1 >= r2
let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) implies r1 >= r2 )
assume that
A34: i <= k + 1 and
A35: i in dom f and
A36: r1 = f . i and
A37: r2 = f . (k + 1) ; ::_thesis: r1 >= r2
percases ( i < k + 1 or i >= k + 1 ) ;
supposeA38: i < k + 1 ; ::_thesis: r1 >= r2
reconsider r3 = f . n1 as Real ;
i <= k by A38, NAT_1:13;
then r1 >= r3 by A5, A35, A36;
hence r1 >= r2 by A24, A37, XXREAL_0:2; ::_thesis: verum
end;
suppose i >= k + 1 ; ::_thesis: r1 >= r2
hence r1 >= r2 by A34, A36, A37, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
A39: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . (k + 1) holds
k + 1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . (k + 1) implies k + 1 <= j )
assume that
j <= k + 1 and
A40: ( j in dom f & f . j = f . (k + 1) ) ; ::_thesis: k + 1 <= j
percases ( j < k + 1 or j >= k + 1 ) ;
suppose j < k + 1 ; ::_thesis: k + 1 <= j
then j <= k by NAT_1:13;
hence k + 1 <= j by A5, A24, A40; ::_thesis: verum
end;
suppose j >= k + 1 ; ::_thesis: k + 1 <= j
hence k + 1 <= j ; ::_thesis: verum
end;
end;
end;
1 <= 1 + k by NAT_1:12;
then ( k + 1 <> 0 implies ( k + 1 <= k + 1 & k + 1 in dom f ) ) by A1, A32, FINSEQ_1:1;
hence S1[k + 1] by A33, A39; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
( ( for i being Element of NAT
for r1, r2 being Real st i <= 0 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 >= r2 ) & ( for j being Element of NAT st j <= 0 & j in dom f & f . j = f . 1 holds
1 <= j ) ) by A1, FINSEQ_1:1;
then A41: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A41, A3);
then consider n1 being Element of NAT such that
A42: ( len f <> 0 implies ( n1 <= len f & n1 in dom f ) ) and
A43: for i being Element of NAT
for 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 Element of NAT st j <= len f & j in dom f & f . j = f . n1 holds
n1 <= j ;
A45: for j being Element of NAT st j in dom f & f . j = f . n1 holds
n1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j in dom f & f . j = f . n1 implies n1 <= j )
assume that
A46: j in dom f and
A47: f . j = f . n1 ; ::_thesis: n1 <= j
j <= len f by A46, FINSEQ_3:25;
hence n1 <= j by A44, A46, A47; ::_thesis: verum
end;
for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
let r1, r2 be Real; ::_thesis: ( i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 )
assume that
A48: i in dom f and
A49: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 >= r2
i <= len f by A48, FINSEQ_3:25;
hence r1 >= r2 by A43, A48, A49; ::_thesis: verum
end;
hence ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) by A2, A42, A45; ::_thesis: verum
end;
end;
end;
hence ex b1 being Element of NAT st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof
thus for m1, m2 being Element of NAT st ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 >= r2 ) & ( for j being Element of 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 Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) holds
m1 = m2 ::_thesis: verum
proof
let m1, m2 be Element of NAT ; ::_thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 >= r2 ) & ( for j being Element of 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 Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) implies m1 = m2 )
assume A50: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 >= r2 ) & ( for j being Element of 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 Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) ) ; ::_thesis: m1 = m2
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 m1 = m2 by XXREAL_0:1; ::_thesis: verum
end;
end;
end;
:: deftheorem Def2 defines min_p RFINSEQ2:def_2_:_
for f being FinSequence of REAL
for b2 being Element of NAT holds
( b2 = min_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );
definition
let f be FinSequence of REAL ;
func max f -> Real equals :: RFINSEQ2:def 3
f . (max_p f);
correctness
coherence
f . (max_p f) is Real;
;
func min f -> Real equals :: RFINSEQ2:def 4
f . (min_p f);
correctness
coherence
f . (min_p f) is Real;
;
end;
:: deftheorem defines max RFINSEQ2:def_3_:_
for f being FinSequence of REAL holds max f = f . (max_p f);
:: deftheorem defines min RFINSEQ2:def_4_:_
for f being FinSequence of REAL holds min f = f . (min_p f);
theorem Th1: :: RFINSEQ2:1
for f being FinSequence of REAL
for i being Element of 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 ; ::_thesis: for i being Element of NAT st 1 <= i & i <= len f holds
( f . i <= f . (max_p f) & f . i <= max f )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len f implies ( f . i <= f . (max_p f) & f . i <= max f ) )
assume A1: ( 1 <= i & i <= len f ) ; ::_thesis: ( f . i <= f . (max_p f) & f . i <= max f )
then A2: i in dom f by FINSEQ_3:25;
hence f . i <= f . (max_p f) by A1, Def1; ::_thesis: f . i <= max f
thus f . i <= max f by A1, A2, Def1; ::_thesis: verum
end;
theorem Th2: :: RFINSEQ2:2
for f being FinSequence of REAL
for i being Element of 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 ; ::_thesis: for i being Element of NAT st 1 <= i & i <= len f holds
( f . i >= f . (min_p f) & f . i >= min f )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len f implies ( f . i >= f . (min_p f) & f . i >= min f ) )
assume A1: ( 1 <= i & i <= len f ) ; ::_thesis: ( f . i >= f . (min_p f) & f . i >= min f )
then A2: i in dom f by FINSEQ_3:25;
hence f . i >= f . (min_p f) by A1, Def2; ::_thesis: f . i >= min f
thus f . i >= min f by A1, A2, Def2; ::_thesis: verum
end;
theorem :: RFINSEQ2:3
for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( max_p f = 1 & max f = r )
proof
let f be FinSequence of REAL ; ::_thesis: for r being Real st f = <*r*> holds
( max_p f = 1 & max f = r )
let r be Real; ::_thesis: ( f = <*r*> implies ( max_p f = 1 & max f = r ) )
assume A1: f = <*r*> ; ::_thesis: ( max_p f = 1 & max 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 ( max_p f = 1 & max f = r ) by A3, A2, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RFINSEQ2:4
for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( min_p f = 1 & min f = r )
proof
let f be FinSequence of REAL ; ::_thesis: for r being Real st f = <*r*> holds
( min_p f = 1 & min f = r )
let r be Real; ::_thesis: ( f = <*r*> implies ( min_p f = 1 & min f = r ) )
assume A1: f = <*r*> ; ::_thesis: ( min_p f = 1 & min 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 ( min_p f = 1 & min f = r ) by A3, A2, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RFINSEQ2:5
for f being FinSequence of REAL
for 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 ; ::_thesis: for r1, r2 being Real st f = <*r1,r2*> holds
( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
let r1, r2 be Real; ::_thesis: ( f = <*r1,r2*> implies ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) )
assume A1: f = <*r1,r2*> ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
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__::_thesis:_(_(_r1_>=_r2_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_or_(_r1_<_r2_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_)
percases ( r1 >= r2 or r1 < r2 ) ;
case r1 >= r2 ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
then A10: max (r1,r2) <= max f by A4, A9, XXREAL_0:def_10;
now__::_thesis:_(_(_max_p_f_<_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_or_(_max_p_f_>=_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_)
percases ( max_p f < len f or max_p f >= len f ) ;
case max_p f < len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
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 ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A4, A11, FUNCOP_1:def_8; ::_thesis: verum
end;
case max_p f >= len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
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 ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A8, A12, A13, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ; ::_thesis: verum
end;
case r1 < r2 ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
then A14: max (r1,r2) <= max f by A8, A3, XXREAL_0:def_10;
now__::_thesis:_(_(_max_p_f_<_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_or_(_max_p_f_>=_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_)
percases ( max_p f < len f or max_p f >= len f ) ;
case max_p f < len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
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 ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A4, A15, FUNCOP_1:def_8; ::_thesis: verum
end;
case max_p f >= len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
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 ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A8, A16, A17, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ; ::_thesis: verum
end;
end;
end;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ; ::_thesis: verum
end;
theorem :: RFINSEQ2:6
for f being FinSequence of REAL
for 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 ; ::_thesis: for r1, r2 being Real st f = <*r1,r2*> holds
( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
let r1, r2 be Real; ::_thesis: ( f = <*r1,r2*> implies ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) )
assume A1: f = <*r1,r2*> ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
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;
percases ( r1 <= r2 or r1 > r2 ) ;
suppose r1 <= r2 ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
then A10: min (r1,r2) >= min f by A8, A3, XXREAL_0:def_9;
now__::_thesis:_(_(_min_p_f_<_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_or_(_min_p_f_>=_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_)
percases ( min_p f < len f or min_p f >= len f ) ;
case min_p f < len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
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 ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A8, A11, FUNCOP_1:def_8; ::_thesis: verum
end;
case min_p f >= len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
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 ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A4, A12, A13, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) ; ::_thesis: verum
end;
suppose r1 > r2 ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
then A14: min (r1,r2) >= min f by A4, A7, XXREAL_0:def_9;
now__::_thesis:_(_(_min_p_f_<_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_or_(_min_p_f_>=_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_)
percases ( min_p f < len f or min_p f >= len f ) ;
case min_p f < len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
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 ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A8, A15, FUNCOP_1:def_8; ::_thesis: verum
end;
case min_p f >= len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
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 ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A4, A16, A17, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) ; ::_thesis: verum
end;
end;
end;
theorem :: RFINSEQ2:7
for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
max (f1 + f2) <= (max f1) + (max f2)
proof
let f1, f2 be FinSequence of REAL ; ::_thesis: ( len f1 = len f2 & len f1 > 0 implies max (f1 + f2) <= (max f1) + (max f2) )
assume that
A1: len f1 = len f2 and
A2: len f1 > 0 ; ::_thesis: max (f1 + f2) <= (max f1) + (max f2)
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 max (f1 + f2) <= (max f1) + (max f2) by A7, A6, XREAL_1:7; ::_thesis: verum
end;
theorem :: RFINSEQ2:8
for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
min (f1 + f2) >= (min f1) + (min f2)
proof
let f1, f2 be FinSequence of REAL ; ::_thesis: ( len f1 = len f2 & len f1 > 0 implies min (f1 + f2) >= (min f1) + (min f2) )
assume that
A1: len f1 = len f2 and
A2: len f1 > 0 ; ::_thesis: min (f1 + f2) >= (min f1) + (min f2)
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 min (f1 + f2) >= (min f1) + (min f2) by A7, A6, XREAL_1:7; ::_thesis: verum
end;
theorem :: RFINSEQ2:9
for f being FinSequence of REAL
for 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 ; ::_thesis: for a being Real st len f > 0 & a > 0 holds
( max (a * f) = a * (max f) & max_p (a * f) = max_p f )
let a be Real; ::_thesis: ( len f > 0 & a > 0 implies ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) )
assume that
A1: len f > 0 and
A2: a > 0 ; ::_thesis: ( max (a * f) = a * (max f) & max_p (a * f) = max_p f )
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 ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) by A11, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RFINSEQ2:10
for f being FinSequence of REAL
for 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 ; ::_thesis: for a being Real st len f > 0 & a > 0 holds
( min (a * f) = a * (min f) & min_p (a * f) = min_p f )
let a be Real; ::_thesis: ( len f > 0 & a > 0 implies ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) )
assume that
A1: len f > 0 and
A2: a > 0 ; ::_thesis: ( min (a * f) = a * (min f) & min_p (a * f) = min_p f )
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 ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) by A11, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RFINSEQ2:11
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 ; ::_thesis: ( len f > 0 implies ( max (- f) = - (min f) & max_p (- f) = min_p f ) )
assume A1: len f > 0 ; ::_thesis: ( max (- f) = - (min f) & max_p (- f) = min_p f )
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 ( max (- f) = - (min f) & max_p (- f) = min_p f ) by A10, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RFINSEQ2:12
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 ; ::_thesis: ( len f > 0 implies ( min (- f) = - (max f) & min_p (- f) = max_p f ) )
assume A1: len f > 0 ; ::_thesis: ( min (- f) = - (max f) & min_p (- f) = max_p f )
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 ( min (- f) = - (max f) & min_p (- f) = max_p f ) by A10, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RFINSEQ2:13
for f being FinSequence of REAL
for n being Element of NAT st n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )
proof
let f be FinSequence of REAL ; ::_thesis: for n being Element of NAT st n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )
let n be Element of NAT ; ::_thesis: ( n < len f implies ( max (f /^ n) <= max f & min (f /^ n) >= min f ) )
A1: 1 <= 1 + n by NAT_1:12;
assume A2: n < len f ; ::_thesis: ( max (f /^ n) <= max f & min (f /^ n) >= min 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 ( max (f /^ n) <= max f & min (f /^ n) >= min f ) by A2, A12, A9, A6, Def1, Def2; ::_thesis: verum
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 ; ::_thesis: ( f,g are_fiberwise_equipotent implies max f <= max g )
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: max f <= max g
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;
percases ( len f > 0 or len f <= 0 ) ;
supposeA5: len f > 0 ; ::_thesis: max f <= max g
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;
then reconsider n = P . (max_p f) as Element of NAT ;
dom g = Seg (len g) by FINSEQ_1:def_3;
then ( 1 <= n & n <= len g ) by A8, FINSEQ_1:1;
hence max f <= max g by A2, A7, Th1; ::_thesis: verum
end;
suppose len f <= 0 ; ::_thesis: max f <= max g
then ( f = {} & g = {} ) by A4;
hence max f <= max g ; ::_thesis: verum
end;
end;
end;
theorem Th14: :: RFINSEQ2:14
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 ; ::_thesis: ( f,g are_fiberwise_equipotent implies max f = max g )
assume f,g are_fiberwise_equipotent ; ::_thesis: max f = max g
then ( max f <= max g & max g <= max f ) by Lm1;
hence max f = max g by XXREAL_0:1; ::_thesis: verum
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 ; ::_thesis: ( f,g are_fiberwise_equipotent implies min f >= min g )
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: min f >= min g
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;
percases ( len f > 0 or len f <= 0 ) ;
supposeA4: len f > 0 ; ::_thesis: min f >= min g
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;
then reconsider n = P . (min_p f) as Element of NAT ;
dom g = Seg (len g) by FINSEQ_1:def_3;
then ( 1 <= n & n <= len g ) by A8, FINSEQ_1:1;
hence min f >= min g by A2, A7, Th2; ::_thesis: verum
end;
suppose len f <= 0 ; ::_thesis: min f >= min g
then ( f = {} & g = {} ) by A3;
hence min f >= min g ; ::_thesis: verum
end;
end;
end;
theorem Th15: :: RFINSEQ2:15
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 ; ::_thesis: ( f,g are_fiberwise_equipotent implies min f = min g )
assume f,g are_fiberwise_equipotent ; ::_thesis: min f = min g
then ( min f >= min g & min g >= min f ) by Lm2;
hence min f = min g by XXREAL_0:1; ::_thesis: verum
end;
definition
let f be FinSequence of REAL ;
func sort_d f -> non-increasing FinSequence of REAL means :Def5: :: RFINSEQ2:def 5
f,it are_fiberwise_equipotent ;
existence
ex b1 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent by RFINSEQ:22;
uniqueness
for b1, b2 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds
b1 = b2 by CLASSES1:76, RFINSEQ:23;
projectivity
for b1 being non-increasing FinSequence of REAL
for b2 being FinSequence of REAL st b2,b1 are_fiberwise_equipotent holds
b1,b1 are_fiberwise_equipotent ;
end;
:: deftheorem Def5 defines sort_d RFINSEQ2:def_5_:_
for f being FinSequence of REAL
for b2 being non-increasing FinSequence of REAL holds
( b2 = sort_d f iff f,b2 are_fiberwise_equipotent );
theorem Th16: :: RFINSEQ2:16
for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds
R is non-decreasing
proof
let R be FinSequence of REAL ; ::_thesis: ( ( len R = 0 or len R = 1 ) implies R is non-decreasing )
assume A1: ( len R = 0 or len R = 1 ) ; ::_thesis: R is non-decreasing
percases ( len R = 0 or len R = 1 ) by A1;
suppose len R = 0 ; ::_thesis: R is non-decreasing
then R = <*> REAL ;
then for n being Element of NAT st n in dom R & n + 1 in dom R holds
R . n <= R . (n + 1) ;
hence R is non-decreasing by INTEGRA2:def_1; ::_thesis: verum
end;
suppose len R = 1 ; ::_thesis: R is non-decreasing
then A2: dom R = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_R_&_n_+_1_in_dom_R_holds_
R_._n_<=_R_._(n_+_1)
let n be Element of NAT ; ::_thesis: ( n in dom R & n + 1 in dom R implies R . n <= R . (n + 1) )
assume that
A3: n in dom R and
A4: n + 1 in dom R ; ::_thesis: R . n <= R . (n + 1)
n = 1 by A2, A3, TARSKI:def_1;
hence R . n <= R . (n + 1) by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
hence R is non-decreasing by INTEGRA2:def_1; ::_thesis: verum
end;
end;
end;
theorem Th17: :: RFINSEQ2:17
for R being FinSequence of REAL holds
( R is non-decreasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m )
proof
let R be FinSequence of REAL ; ::_thesis: ( R is non-decreasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m )
thus ( R is non-decreasing implies for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m ) ::_thesis: ( ( for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m ) implies R is non-decreasing )
proof
defpred S1[ Element of NAT ] means ( $1 in dom R implies for n being Element of NAT st n in dom R & n < $1 holds
R . n <= R . $1 );
assume A1: R is non-decreasing ; ::_thesis: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m
A2: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; ::_thesis: S1[m + 1]
assume A4: m + 1 in dom R ; ::_thesis: for n being Element of NAT st n in dom R & n < m + 1 holds
R . n <= R . (m + 1)
then m + 1 <= len R by FINSEQ_3:25;
then A5: m <= len R by NAT_1:13;
let n be Element of NAT ; ::_thesis: ( n in dom R & n < m + 1 implies R . n <= R . (m + 1) )
assume that
A6: n in dom R and
A7: n < m + 1 ; ::_thesis: R . n <= R . (m + 1)
set t = R . m;
set r = R . n;
set 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__::_thesis:_(_(_n_=_m_&_R_._n_<=_R_._(m_+_1)_)_or_(_n_<>_m_&_R_._n_<=_R_._(m_+_1)_)_)
percases ( n = m or n <> m ) ;
case n = m ; ::_thesis: R . n <= R . (m + 1)
hence R . n <= R . (m + 1) by A1, A4, A6, INTEGRA2:def_1; ::_thesis: verum
end;
case n <> m ; ::_thesis: R . n <= R . (m + 1)
then n < m by A8, XXREAL_0:1;
then A11: R . n <= R . m by A3, A6, A9, A5, FINSEQ_3:25;
R . m <= R . (m + 1) by A1, A4, A10, INTEGRA2:def_1;
hence R . n <= R . (m + 1) by A11, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence R . n <= R . (m + 1) ; ::_thesis: verum
end;
A12: S1[ 0 ] ;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A12, A2);
hence for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m ; ::_thesis: verum
end;
assume A13: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m ; ::_thesis: R is non-decreasing
let n be Element of NAT ; :: according to INTEGRA2:def_1 ::_thesis: ( not n in dom R or not n + 1 in dom R or R . n <= R . (n + 1) )
A14: n < n + 1 by NAT_1:13;
assume ( n in dom R & n + 1 in dom R ) ; ::_thesis: R . n <= R . (n + 1)
hence R . n <= R . (n + 1) by A13, A14; ::_thesis: verum
end;
Lm3: for f, g being non-decreasing FinSequence of REAL
for n being Element of NAT 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 ; ::_thesis: for n being Element of NAT 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 )
let n be Element of NAT ; ::_thesis: ( len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent implies ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) )
assume that
A1: len f = n + 1 and
A2: len f = len g and
A3: f,g are_fiberwise_equipotent ; ::_thesis: ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
set r = f . (n + 1);
set 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) ^ <*(f . (n + 1))*> by A1, RFINSEQ:7;
A7: n + 1 in dom g by A1, A2, A4, FINSEQ_3:25;
A8: now__::_thesis:_not_f_._(n_+_1)_<>_g_._(n_+_1)
A9: rng f = rng g by A3, CLASSES1:75;
assume A10: f . (n + 1) <> g . (n + 1) ; ::_thesis: contradiction
now__::_thesis:_(_(_f_._(n_+_1)_<_g_._(n_+_1)_&_contradiction_)_or_(_f_._(n_+_1)_>_g_._(n_+_1)_&_contradiction_)_)
percases ( f . (n + 1) < g . (n + 1) or f . (n + 1) > g . (n + 1) ) by A10, XXREAL_0:1;
caseA11: f . (n + 1) < g . (n + 1) ; ::_thesis: contradiction
g . (n + 1) 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 = g . (n + 1) by FINSEQ_2:10;
A14: m <= len f by A12, FINSEQ_3:25;
now__::_thesis:_(_(_m_=_len_f_&_contradiction_)_or_(_m_<>_len_f_&_contradiction_)_)
percases ( m = len f or m <> len f ) ;
case m = len f ; ::_thesis: contradiction
hence contradiction by A1, A11, A13; ::_thesis: verum
end;
case m <> len f ; ::_thesis: contradiction
then m < n + 1 by A1, A14, XXREAL_0:1;
hence contradiction by A5, A11, A12, A13, Th17; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
caseA15: f . (n + 1) > g . (n + 1) ; ::_thesis: contradiction
f . (n + 1) 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 = f . (n + 1) by FINSEQ_2:10;
A18: m <= len g by A16, FINSEQ_3:25;
now__::_thesis:_(_(_m_=_len_g_&_contradiction_)_or_(_m_<>_len_g_&_contradiction_)_)
percases ( m = len g or m <> len g ) ;
case m = len g ; ::_thesis: contradiction
hence contradiction by A1, A2, A15, A17; ::_thesis: verum
end;
case m <> len g ; ::_thesis: contradiction
then m < n + 1 by A1, A2, A18, XXREAL_0:1;
hence contradiction by A7, A15, A16, A17, Th17; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence f . (len f) = g . (len g) by A1, A2; ::_thesis: f | n,g | n are_fiberwise_equipotent
A19: g = (g | n) ^ <*(f . (n + 1))*> by A1, A2, A8, RFINSEQ:7;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_((g_|_n),x))
let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim ((g | n),x))
(card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) = card (Coim (f,x)) by A6, FINSEQ_3:57
.= card (Coim (g,x)) by A3, CLASSES1:def_9
.= (card ((g | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) by A19, FINSEQ_3:57 ;
hence card (Coim ((f | n),x)) = card (Coim ((g | n),x)) ; ::_thesis: verum
end;
hence f | n,g | n are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
theorem Th18: :: RFINSEQ2:18
for R being non-decreasing FinSequence of REAL
for n being Element of NAT holds R | n is non-decreasing FinSequence of REAL
proof
let f be non-decreasing FinSequence of REAL ; ::_thesis: for n being Element of NAT holds f | n is non-decreasing FinSequence of REAL
let n be Element of NAT ; ::_thesis: f | n is non-decreasing FinSequence of REAL
set fn = f | n;
now__::_thesis:_(_(_n_=_0_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_or_(_n_<>_0_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: f | n is non-decreasing FinSequence of REAL
then len (f | n) = 0 ;
hence f | n is non-decreasing FinSequence of REAL by Th16; ::_thesis: verum
end;
case n <> 0 ; ::_thesis: f | n is non-decreasing FinSequence of REAL
then A1: 0 + 1 <= n by NAT_1:13;
now__::_thesis:_(_(_len_f_<=_n_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_or_(_n_<_len_f_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_)
percases ( len f <= n or n < len f ) ;
case len f <= n ; ::_thesis: f | n is non-decreasing FinSequence of REAL
hence f | n is non-decreasing FinSequence of REAL by FINSEQ_1:58; ::_thesis: verum
end;
case n < len f ; ::_thesis: f | n is non-decreasing FinSequence of REAL
then A2: ( n in dom f & len (f | n) = n ) by A1, FINSEQ_1:59, FINSEQ_3:25;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_|_n)_&_m_+_1_in_dom_(f_|_n)_holds_
(f_|_n)_._m_<=_(f_|_n)_._(m_+_1)
let m be Element of NAT ; ::_thesis: ( m in dom (f | n) & m + 1 in dom (f | n) implies (f | n) . m <= (f | n) . (m + 1) )
A3: dom (f | n) = Seg (len (f | n)) by FINSEQ_1:def_3;
assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; ::_thesis: (f | n) . m <= (f | n) . (m + 1)
then A5: ( m in dom f & m + 1 in dom f ) by A2, A3, RFINSEQ:6;
( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, RFINSEQ:6;
hence (f | n) . m <= (f | n) . (m + 1) by A5, INTEGRA2:def_1; ::_thesis: verum
end;
hence f | n is non-decreasing FinSequence of REAL by INTEGRA2:def_1; ::_thesis: verum
end;
end;
end;
hence f | n is non-decreasing FinSequence of REAL ; ::_thesis: verum
end;
end;
end;
hence f | n is non-decreasing FinSequence of REAL ; ::_thesis: verum
end;
Lm4: for n being Element of NAT
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
proof
defpred S1[ Element of NAT ] means for g1, g2 being non-decreasing FinSequence of REAL st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let g1, g2 be non-decreasing FinSequence of REAL ; ::_thesis: ( n + 1 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 )
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 ; ::_thesis: g1 = g2
A5: len g2 = len g1 by A4, RFINSEQ:3;
then A6: g1 . (len g1) = g2 . (len g2) by A3, A4, Lm3;
A7: (g1 | n) ^ <*(g1 . (n + 1))*> = 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 g1 = g2 by A3, A5, A6, A7, RFINSEQ:7; ::_thesis: verum
end;
A8: S1[ 0 ]
proof
let g1, g2 be non-decreasing FinSequence of REAL ; ::_thesis: ( 0 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 )
assume ( len g1 = 0 & g1,g2 are_fiberwise_equipotent ) ; ::_thesis: g1 = g2
then ( len g2 = len g1 & g1 = <*> REAL ) by RFINSEQ:3;
hence g1 = g2 ; ::_thesis: verum
end;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A8, A1);
hence for n being Element of NAT
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2 ; ::_thesis: verum
end;
theorem Th19: :: RFINSEQ2:19
for R1, R2 being non-decreasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
R1 = R2
proof
let g1, g2 be non-decreasing FinSequence of REAL ; ::_thesis: ( g1,g2 are_fiberwise_equipotent implies g1 = g2 )
A1: len g1 = len g1 ;
assume g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2
hence g1 = g2 by A1, Lm4; ::_thesis: verum
end;
definition
let f be FinSequence of REAL ;
func sort_a f -> non-decreasing FinSequence of REAL means :Def6: :: RFINSEQ2:def 6
f,it are_fiberwise_equipotent ;
existence
ex b1 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent by INTEGRA2:3;
uniqueness
for b1, b2 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds
b1 = b2 by Th19, CLASSES1:76;
projectivity
for b1 being non-decreasing FinSequence of REAL
for b2 being FinSequence of REAL st b2,b1 are_fiberwise_equipotent holds
b1,b1 are_fiberwise_equipotent ;
end;
:: deftheorem Def6 defines sort_a RFINSEQ2:def_6_:_
for f being FinSequence of REAL
for b2 being non-decreasing FinSequence of REAL holds
( b2 = sort_a f iff f,b2 are_fiberwise_equipotent );
theorem :: RFINSEQ2:20
for f being non-increasing FinSequence of REAL holds sort_d f = f by Def5;
theorem :: RFINSEQ2:21
for f being non-decreasing FinSequence of REAL holds sort_a f = f by Def6;
theorem :: RFINSEQ2:22
canceled;
theorem :: RFINSEQ2:23
canceled;
theorem Th24: :: RFINSEQ2:24
for f being FinSequence of REAL st f is non-increasing holds
- f is non-decreasing
proof
let f be FinSequence of REAL ; ::_thesis: ( f is non-increasing implies - f is non-decreasing )
assume A1: f is non-increasing ; ::_thesis: - f is non-decreasing
for n being Element of NAT st n in dom (- f) & n + 1 in dom (- f) holds
(- f) . n <= (- f) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( n in dom (- f) & n + 1 in dom (- f) implies (- f) . n <= (- f) . (n + 1) )
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) ) ; ::_thesis: (- f) . n <= (- f) . (n + 1)
then f . n >= f . (n + 1) by A1, A2, RFINSEQ:def_3;
hence (- f) . n <= (- f) . (n + 1) by A3, XREAL_1:24; ::_thesis: verum
end;
hence - f is non-decreasing by INTEGRA2:def_1; ::_thesis: verum
end;
theorem Th25: :: RFINSEQ2:25
for f being FinSequence of REAL st f is non-decreasing holds
- f is non-increasing
proof
let f be FinSequence of REAL ; ::_thesis: ( f is non-decreasing implies - f is non-increasing )
assume A1: f is non-decreasing ; ::_thesis: - f is non-increasing
for n being Element of NAT st n in dom (- f) & n + 1 in dom (- f) holds
(- f) . n >= (- f) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( n in dom (- f) & n + 1 in dom (- f) implies (- f) . n >= (- f) . (n + 1) )
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) ) ; ::_thesis: (- f) . n >= (- f) . (n + 1)
then f . n <= f . (n + 1) by A1, A2, INTEGRA2:def_1;
hence (- f) . n >= (- f) . (n + 1) by A3, XREAL_1:24; ::_thesis: verum
end;
hence - f is non-increasing by RFINSEQ:def_3; ::_thesis: verum
end;
theorem Th26: :: RFINSEQ2:26
for f, g being FinSequence of REAL
for 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 ; ::_thesis: for P being Permutation of (dom g) st f = g * P & len g >= 1 holds
- f = (- g) * P
let P be Permutation of (dom g); ::_thesis: ( f = g * P & len g >= 1 implies - f = (- g) * P )
assume that
A1: f = g * P and
A2: len g >= 1 ; ::_thesis: - f = (- g) * P
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; ::_thesis: ( i in dom (- f) implies (- f) . i = k . i )
assume A10: i in dom (- f) ; ::_thesis: (- f) . i = k . i
then P . i in rng P by A7, FUNCT_1:3;
then reconsider j = P . i as Element of NAT by A3;
(- 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 (- f) . i = k . i ; ::_thesis: verum
end;
hence - f = (- g) * P by A8, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th27: :: RFINSEQ2:27
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 ; ::_thesis: ( f,g are_fiberwise_equipotent implies - f, - g are_fiberwise_equipotent )
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: - f, - g are_fiberwise_equipotent
then consider P being Permutation of (dom g) such that
A2: f = g * P by RFINSEQ:4;
A3: now__::_thesis:_(_(_len_g_>=_1_&_-_f_=_(-_g)_*_P_)_or_(_len_g_<_1_&_-_f_=_(-_g)_*_P_)_)
percases ( len g >= 1 or len g < 1 ) ;
case len g >= 1 ; ::_thesis: - f = (- g) * P
hence - f = (- g) * P by A2, Th26; ::_thesis: verum
end;
case len g < 1 ; ::_thesis: - f = (- g) * P
then A4: len g < 0 + 1 ;
then A5: g = {} by NAT_1:13;
len g = 0 by A4, NAT_1:13;
then A6: len f = 0 by A1, RFINSEQ:3;
then len (- f) = 0 by RVSUM_1:114;
then A7: - f = {} ;
f = {} by A6;
hence - f = (- g) * P by A2, A5, A7; ::_thesis: verum
end;
end;
end;
dom (- g) = dom g by VALUED_1:8;
hence - f, - g are_fiberwise_equipotent by A3, RFINSEQ:4; ::_thesis: verum
end;
theorem :: RFINSEQ2:28
for f being FinSequence of REAL holds sort_d (- f) = - (sort_a f)
proof
let f be FinSequence of REAL ; ::_thesis: sort_d (- f) = - (sort_a f)
- f, sort_d (- f) are_fiberwise_equipotent by Def5;
then A1: - (- f), - (sort_d (- f)) are_fiberwise_equipotent by Th27;
- (sort_d (- f)) is non-decreasing by Th24;
then - (sort_d (- f)) = sort_a f by A1, Def6;
hence sort_d (- f) = - (sort_a f) ; ::_thesis: verum
end;
theorem :: RFINSEQ2:29
for f being FinSequence of REAL holds sort_a (- f) = - (sort_d f)
proof
let f be FinSequence of REAL ; ::_thesis: sort_a (- f) = - (sort_d f)
- f, sort_a (- f) are_fiberwise_equipotent by Def6;
then A1: - (- f), - (sort_a (- f)) are_fiberwise_equipotent by Th27;
- (sort_a (- f)) is non-increasing by Th25;
then - (sort_a (- f)) = sort_d f by A1, Def5;
hence sort_a (- f) = - (sort_d f) ; ::_thesis: verum
end;
theorem Th30: :: RFINSEQ2:30
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 ; ::_thesis: ( dom (sort_d f) = dom f & len (sort_d f) = len f )
f, sort_d f are_fiberwise_equipotent by Def5;
hence ( dom (sort_d f) = dom f & len (sort_d f) = len f ) by RFINSEQ:3; ::_thesis: verum
end;
theorem Th31: :: RFINSEQ2:31
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 ; ::_thesis: ( dom (sort_a f) = dom f & len (sort_a f) = len f )
f, sort_a f are_fiberwise_equipotent by Def6;
hence ( dom (sort_a f) = dom f & len (sort_a f) = len f ) by RFINSEQ:3; ::_thesis: verum
end;
theorem :: RFINSEQ2:32
for f being FinSequence of REAL st len f >= 1 holds
( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f )
proof
let f be FinSequence of REAL ; ::_thesis: ( len f >= 1 implies ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) )
assume A1: len f >= 1 ; ::_thesis: ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f )
A2: len (sort_d f) = len f by Th30;
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 Element of NAT
for 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 Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 holds
r1 <= r2
let r1, r2 be Real; ::_thesis: ( i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 implies r1 <= r2 )
assume that
A5: i in dom (sort_d f) and
A6: ( r1 = (sort_d f) . i & r2 = (sort_d f) . 1 ) ; ::_thesis: r1 <= r2
i in Seg (len (sort_d f)) by A5, FINSEQ_1:def_3;
then A7: 1 <= i by FINSEQ_1:1;
now__::_thesis:_(_(_1_=_i_&_r1_<=_r2_)_or_(_1_<>_i_&_r1_<=_r2_)_)
percases ( 1 = i or 1 <> i ) ;
case 1 = i ; ::_thesis: r1 <= r2
hence r1 <= r2 by A6; ::_thesis: verum
end;
case 1 <> i ; ::_thesis: r1 <= r2
then 1 < i by A7, XXREAL_0:1;
hence r1 <= r2 by A3, A5, A6, RFINSEQ:19; ::_thesis: verum
end;
end;
end;
hence r1 <= r2 ; ::_thesis: verum
end;
A8: len (sort_a f) = len f by Th31;
then A9: 1 in dom (sort_a f) by A1, FINSEQ_3:25;
A10: for i being Element of NAT
for 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 Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 holds
r1 >= r2
let r1, r2 be Real; ::_thesis: ( i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 implies r1 >= r2 )
assume that
A11: i in dom (sort_a f) and
A12: ( r1 = (sort_a f) . i & r2 = (sort_a f) . 1 ) ; ::_thesis: r1 >= r2
A13: 1 <= i by A11, FINSEQ_3:25;
percases ( 1 = i or 1 <> i ) ;
suppose 1 = i ; ::_thesis: r1 >= r2
hence r1 >= r2 by A12; ::_thesis: verum
end;
suppose 1 <> i ; ::_thesis: r1 >= r2
then 1 < i by A13, XXREAL_0:1;
hence r1 >= r2 by A9, A11, A12, Th17; ::_thesis: verum
end;
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 Element of 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 Element of NAT st j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 holds
1 <= j
proof
let j be Element of NAT ; ::_thesis: ( j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 implies 1 <= j )
assume that
A19: j in dom (sort_d f) and
(sort_d f) . j = (sort_d f) . 1 ; ::_thesis: 1 <= j
j in Seg (len (sort_d f)) by A19, FINSEQ_1:def_3;
hence 1 <= j by FINSEQ_1:1; ::_thesis: verum
end;
then (sort_d f) . 1 = max (sort_d f) by A1, A2, A3, A4, Def1
.= max f by A15, Th14 ;
hence ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) by A1, A2, A3, A4, A18, A8, A9, A10, A16, A17, Def1, Def2; ::_thesis: verum
end;