:: by Yatsuka Nakamura

::

:: Received October 17, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

definition

let f be FinSequence of REAL ;

ex b_{1} being Nat st

( ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) )

for b_{1}, b_{2} being Nat st ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) & ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) holds

b_{1} = b_{2}

end;
func max_p f -> Nat means :Def1: :: RFINSEQ2:def 1

( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for 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 ( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for 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 ) ) ) );

ex b

( ( len f = 0 implies b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

proof end;

uniqueness for b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

b

proof end;

:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :

for f being FinSequence of REAL

for b_{2} being Nat holds

( b_{2} = max_p f iff ( ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) ) );

for f being FinSequence of REAL

for b

( b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

definition

let f be FinSequence of REAL ;

ex b_{1} being Nat st

( ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) )

for b_{1}, b_{2} being Nat st ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) & ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) holds

b_{1} = b_{2}

end;
func min_p f -> Nat means :Def2: :: RFINSEQ2:def 2

( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for 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 ( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for 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 ) ) ) );

ex b

( ( len f = 0 implies b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

proof end;

uniqueness for b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

b

proof end;

:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :

for f being FinSequence of REAL

for b_{2} being Nat holds

( b_{2} = min_p f iff ( ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) ) );

for f being FinSequence of REAL

for b

( b

for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

definition

let f be FinSequence of REAL ;

correctness

coherence

f . (max_p f) is Real;

;

correctness

coherence

f . (min_p f) is Real;

;

end;
correctness

coherence

f . (max_p f) is Real;

;

correctness

coherence

f . (min_p f) is Real;

;

:: deftheorem defines max RFINSEQ2:def 3 :

for f being FinSequence of REAL holds max f = f . (max_p f);

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);

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 Nat st 1 <= i & i <= len f holds

( f . i <= f . (max_p f) & f . i <= max f )

for i being Nat st 1 <= i & i <= len f holds

( f . i <= f . (max_p f) & f . i <= max f )

proof end;

theorem Th2: :: RFINSEQ2:2

for f being FinSequence of REAL

for i being Nat st 1 <= i & i <= len f holds

( f . i >= f . (min_p f) & f . i >= min f )

for i being Nat st 1 <= i & i <= len f holds

( f . i >= f . (min_p f) & f . i >= min f )

proof 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) )

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 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) )

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 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)

max (f1 + f2) <= (max f1) + (max f2)

proof 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)

min (f1 + f2) >= (min f1) + (min f2)

proof 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 )

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 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 )

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 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 )

( max (- f) = - (min f) & max_p (- f) = min_p f )

proof 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 )

( min (- f) = - (max f) & min_p (- f) = max_p f )

proof end;

theorem :: RFINSEQ2:13

for f being FinSequence of REAL

for n being Nat st n < len f holds

( max (f /^ n) <= max f & min (f /^ n) >= min f )

for n being Nat st n < len f holds

( max (f /^ n) <= max f & min (f /^ n) >= min f )

proof end;

Lm1: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds

max f <= max g

proof end;

Lm2: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds

min f >= min g

proof end;

definition

let f be FinSequence of REAL ;

ex b_{1} being non-increasing FinSequence of REAL st f,b_{1} are_fiberwise_equipotent
by RFINSEQ:22;

uniqueness

for b_{1}, b_{2} being non-increasing FinSequence of REAL st f,b_{1} are_fiberwise_equipotent & f,b_{2} are_fiberwise_equipotent holds

b_{1} = b_{2}
by CLASSES1:76, RFINSEQ:23;

projectivity

for b_{1} being non-increasing FinSequence of REAL

for b_{2} being FinSequence of REAL st b_{2},b_{1} are_fiberwise_equipotent holds

b_{1},b_{1} are_fiberwise_equipotent
;

end;
::Descend Sorting or Rearrangement of FinSequences

func sort_d f -> non-increasing FinSequence of REAL means :Def5: :: RFINSEQ2:def 5

f,it are_fiberwise_equipotent ;

existence f,it are_fiberwise_equipotent ;

ex b

uniqueness

for b

b

projectivity

for b

for b

b

:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :

for f being FinSequence of REAL

for b_{2} being non-increasing FinSequence of REAL holds

( b_{2} = sort_d f iff f,b_{2} are_fiberwise_equipotent );

for f being FinSequence of REAL

for b

( b

theorem Th17: :: RFINSEQ2:17

for R being FinSequence of REAL holds

( R is non-decreasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds

R . n <= R . m )

( R is non-decreasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds

R . n <= R . m )

proof end;

Lm3: for f, g being non-decreasing FinSequence of REAL

for n being 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 end;

theorem Th18: :: RFINSEQ2:18

for R being non-decreasing FinSequence of REAL

for n being Nat holds R | n is non-decreasing FinSequence of REAL

for n being Nat holds R | n is non-decreasing FinSequence of REAL

proof end;

Lm4: for n being Nat

for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds

g1 = g2

proof end;

definition

let f be FinSequence of REAL ;

ex b_{1} being non-decreasing FinSequence of REAL st f,b_{1} are_fiberwise_equipotent
by INTEGRA2:3;

uniqueness

for b_{1}, b_{2} being non-decreasing FinSequence of REAL st f,b_{1} are_fiberwise_equipotent & f,b_{2} are_fiberwise_equipotent holds

b_{1} = b_{2}
by Th19, CLASSES1:76;

projectivity

for b_{1} being non-decreasing FinSequence of REAL

for b_{2} being FinSequence of REAL st b_{2},b_{1} are_fiberwise_equipotent holds

b_{1},b_{1} are_fiberwise_equipotent
;

end;
::Ascend Sorting or Rearrangement of FinSequences

func sort_a f -> non-decreasing FinSequence of REAL means :Def6: :: RFINSEQ2:def 6

f,it are_fiberwise_equipotent ;

existence f,it are_fiberwise_equipotent ;

ex b

uniqueness

for b

b

projectivity

for b

for b

b

:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :

for f being FinSequence of REAL

for b_{2} being non-decreasing FinSequence of REAL holds

( b_{2} = sort_a f iff f,b_{2} are_fiberwise_equipotent );

for f being FinSequence of REAL

for b

( b

::$CT 2

theorem Th24: :: 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

for P being Permutation of (dom g) st f = g * P & len g >= 1 holds

- f = (- g) * P

proof end;

theorem Th25: :: RFINSEQ2:27

for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds

- f, - g are_fiberwise_equipotent

- f, - g are_fiberwise_equipotent

proof 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 )

( 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 end;