:: RFINSEQ2 semantic presentation

definition

let c₁ be FinSequence of REAL ;
func max_p c₁ -> Nat means :Def1: :: RFINSEQ2:def 1
( ( len a₁ = 0 implies a₂ = 0 ) & ( len a₁ > 0 implies ( a₂ in dom a₁ & ( for b₁ being Nat
for b₂, b₃ being Real st b₁ in dom a₁ & b₂ = a₁ . b₁ & b₃ = a₁ . a₂ holds
b₂ <= b₃ ) & ( for b₁ being Nat st b₁ in dom a₁ & a₁ . b₁ = a₁ . a₂ holds
a₂ <= b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :

definition

let c₁ be FinSequence of REAL ;
func min_p c₁ -> Nat means :Def2: :: RFINSEQ2:def 2
( ( len a₁ = 0 implies a₂ = 0 ) & ( len a₁ > 0 implies ( a₂ in dom a₁ & ( for b₁ being Nat
for b₂, b₃ being Real st b₁ in dom a₁ & b₂ = a₁ . b₁ & b₃ = a₁ . a₂ holds
b₂ >= b₃ ) & ( for b₁ being Nat st b₁ in dom a₁ & a₁ . b₁ = a₁ . a₂ holds
a₂ <= b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :

definition

let c₁ be FinSequence of REAL ;
func max c₁ -> Real equals :: RFINSEQ2:def 3
a₁ . (max_p a₁);
correctness ;
func min c₁ -> Real equals :: RFINSEQ2:def 4
a₁ . (min_p a₁);
correctness ;

end;

:: deftheorem Def3 defines max RFINSEQ2:def 3 :

:: deftheorem Def4 defines min RFINSEQ2:def 4 :

theorem Th1: :: RFINSEQ2:1

for b₁ being FinSequence of REAL
for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
( b₁ . b₂ <= b₁ . (max_p b₁) & b₁ . b₂ <= max b₁ )

proof end;

theorem Th2: :: RFINSEQ2:2

for b₁ being FinSequence of REAL
for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
( b₁ . b₂ >= b₁ . (min_p b₁) & b₁ . b₂ >= min b₁ )

proof end;

theorem Th3: :: RFINSEQ2:3

for b₁ being FinSequence of REAL
for b₂ being Real st b₁ = <*b₂*> holds
( max_p b₁ = 1 & max b₁ = b₂ )

proof end;

theorem Th4: :: RFINSEQ2:4

for b₁ being FinSequence of REAL
for b₂ being Real st b₁ = <*b₂*> holds
( min_p b₁ = 1 & min b₁ = b₂ )

proof end;

theorem Th5: :: RFINSEQ2:5

for b₁ being FinSequence of REAL
for b₂, b₃ being Real st b₁ = <*b₂,b₃*> holds
( max b₁ = max b₂,b₃ & max_p b₁ = IFEQ b₂,(max b₂,b₃),1,2 )

proof end;

theorem Th6: :: RFINSEQ2:6

for b₁ being FinSequence of REAL
for b₂, b₃ being Real st b₁ = <*b₂,b₃*> holds
( min b₁ = min b₂,b₃ & min_p b₁ = IFEQ b₂,(min b₂,b₃),1,2 )

proof end;

theorem Th7: :: RFINSEQ2:7

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ & len b₁ > 0 holds
max (b₁ + b₂) <= (max b₁) + (max b₂)

proof end;

theorem Th8: :: RFINSEQ2:8

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ & len b₁ > 0 holds
min (b₁ + b₂) >= (min b₁) + (min b₂)

proof end;

theorem Th9: :: RFINSEQ2:9

for b₁ being FinSequence of REAL
for b₂ being Real st len b₁ > 0 & b₂ > 0 holds
( max (b₂ * b₁) = b₂ * (max b₁) & max_p (b₂ * b₁) = max_p b₁ )

proof end;

theorem Th10: :: RFINSEQ2:10

for b₁ being FinSequence of REAL
for b₂ being Real st len b₁ > 0 & b₂ > 0 holds
( min (b₂ * b₁) = b₂ * (min b₁) & min_p (b₂ * b₁) = min_p b₁ )

proof end;

theorem Th11: :: RFINSEQ2:11

for b₁ being FinSequence of REAL st len b₁ > 0 holds
( max (- b₁) = - (min b₁) & max_p (- b₁) = min_p b₁ )

proof end;

theorem Th12: :: RFINSEQ2:12

for b₁ being FinSequence of REAL st len b₁ > 0 holds
( min (- b₁) = - (max b₁) & min_p (- b₁) = max_p b₁ )

proof end;

theorem Th13: :: RFINSEQ2:13

for b₁ being FinSequence of REAL
for b₂ being Nat st 1 <= b₂ & b₂ < len b₁ holds
( max (b₁ /^ b₂) <= max b₁ & min (b₁ /^ b₂) >= min b₁ )

proof end;

Lemma5: for b₁, b₂ being FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
max b₁ <= max b₂

proof end;

theorem Th14: :: RFINSEQ2:14

for b₁, b₂ being FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
max b₁ = max b₂

proof end;

Lemma7: for b₁, b₂ being FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
min b₁ >= min b₂

proof end;

theorem Th15: :: RFINSEQ2:15

for b₁, b₂ being FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
min b₁ = min b₂

proof end;

definition

let c₁ be FinSequence of REAL ;
func sort_d c₁ -> non-increasing FinSequence of REAL means :Def5: :: RFINSEQ2:def 5
a₁,a₂ are_fiberwise_equipotent ;
existence by RFINSEQ:35;
uniqueness

proof end;

end;

:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :

theorem Th16: :: RFINSEQ2:16

for b₁ being FinSequence of REAL st ( len b₁ = 0 or len b₁ = 1 ) holds
b₁ is non-decreasing

proof end;

theorem Th17: :: RFINSEQ2:17

for b₁ being FinSequence of REAL holds
( b₁ is non-decreasing iff for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & b₂ < b₃ holds
b₁ . b₂ <= b₁ . b₃ )

proof end;

Lemma12: for b₁, b₂ being non-decreasing FinSequence of REAL
for b₃ being Nat st len b₁ = b₃ + 1 & len b₁ = len b₂ & b₁,b₂ are_fiberwise_equipotent holds
( b₁ . (len b₁) = b₂ . (len b₂) & b₁ | b₃,b₂ | b₃ are_fiberwise_equipotent )

proof end;

theorem Th18: :: RFINSEQ2:18

for b₁ being non-decreasing FinSequence of REAL
for b₂ being Nat holds b₁ | b₂ is non-decreasing FinSequence of REAL

proof end;

Lemma14: for b₁ being Nat
for b₂, b₃ being non-decreasing FinSequence of REAL st b₁ = len b₂ & b₂,b₃ are_fiberwise_equipotent holds
b₂ = b₃

proof end;

theorem Th19: :: RFINSEQ2:19

for b₁, b₂ being non-decreasing FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
b₁ = b₂

proof end;

definition

let c₁ be FinSequence of REAL ;
func sort_a c₁ -> non-decreasing FinSequence of REAL means :Def6: :: RFINSEQ2:def 6
a₁,a₂ are_fiberwise_equipotent ;
existence by INTEGRA2:3;
uniqueness

proof end;

end;

:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :

theorem Th20: :: RFINSEQ2:20

for b₁ being non-increasing FinSequence of REAL holds sort_d b₁ = b₁ by Def5;

theorem Th21: :: RFINSEQ2:21

for b₁ being non-decreasing FinSequence of REAL holds sort_a b₁ = b₁ by Def6;

theorem Th22: :: RFINSEQ2:22

for b₁ being FinSequence of REAL holds sort_d (sort_d b₁) = sort_d b₁ by Def5;

theorem Th23: :: RFINSEQ2:23

for b₁ being FinSequence of REAL holds sort_a (sort_a b₁) = sort_a b₁ by Def6;

theorem Th24: :: RFINSEQ2:24

for b₁ being FinSequence of REAL st b₁ is non-increasing holds
- b₁ is non-decreasing

proof end;

theorem Th25: :: RFINSEQ2:25

for b₁ being FinSequence of REAL st b₁ is non-decreasing holds
- b₁ is non-increasing

proof end;

theorem Th26: :: RFINSEQ2:26

for b₁, b₂ being FinSequence of REAL
for b₃ being Permutation of dom b₂ st b₁ = b₂ * b₃ & len b₂ >= 1 holds
- b₁ = (- b₂) * b₃

proof end;

theorem Th27: :: RFINSEQ2:27

for b₁, b₂ being FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
- b₁, - b₂ are_fiberwise_equipotent

proof end;

theorem Th28: :: RFINSEQ2:28

for b₁ being FinSequence of REAL holds sort_d (- b₁) = - (sort_a b₁)

proof end;

theorem Th29: :: RFINSEQ2:29

for b₁ being FinSequence of REAL holds sort_a (- b₁) = - (sort_d b₁)

proof end;

theorem Th30: :: RFINSEQ2:30

for b₁ being FinSequence of REAL holds
( dom (sort_d b₁) = dom b₁ & len (sort_d b₁) = len b₁ )

proof end;

theorem Th31: :: RFINSEQ2:31

for b₁ being FinSequence of REAL holds
( dom (sort_a b₁) = dom b₁ & len (sort_a b₁) = len b₁ )

proof end;

theorem Th32: :: RFINSEQ2:32

for b₁ being FinSequence of REAL st len b₁ >= 1 holds
( max_p (sort_d b₁) = 1 & min_p (sort_a b₁) = 1 & (sort_d b₁) . 1 = max b₁ & (sort_a b₁) . 1 = min b₁ )

proof end;