:: RFUNCT_3 semantic presentation

definition

let c₁, c₂ be Nat;
redefine func min as min c₁,c₂ -> Nat;
coherence by FINSEQ_2:1;

end;

definition

let c₁ be real number ;
func max+ c₁ -> Real equals :: RFUNCT_3:def 1
max a₁,0;
correctness by XREAL_0:def 1;
func max- c₁ -> Real equals :: RFUNCT_3:def 2
max (- a₁),0;
correctness by XREAL_0:def 1;

end;

:: deftheorem Def1 defines max+ RFUNCT_3:def 1 :

:: deftheorem Def2 defines max- RFUNCT_3:def 2 :

theorem Th1: :: RFUNCT_3:1

for b₁ being real number holds b₁ = (max+ b₁) - (max- b₁)

proof end;

theorem Th2: :: RFUNCT_3:2

for b₁ being real number holds abs b₁ = (max+ b₁) + (max- b₁)

proof end;

theorem Th3: :: RFUNCT_3:3

for b₁ being real number holds 2 * (max+ b₁) = b₁ + (abs b₁)

proof end;

theorem Th4: :: RFUNCT_3:4

for b₁, b₂ being real number st 0 <= b₁ holds
max+ (b₁ * b₂) = b₁ * (max+ b₂)

proof end;

theorem Th5: :: RFUNCT_3:5

for b₁, b₂ being real number holds max+ (b₁ + b₂) <= (max+ b₁) + (max+ b₂)

proof end;

theorem Th6: :: RFUNCT_3:6

for b₁ being real number holds
( 0 <= max+ b₁ & 0 <= max- b₁ ) by SQUARE_1:46;

theorem Th7: :: RFUNCT_3:7

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₃ & b₂ <= b₄ holds
max b₁,b₂ <= max b₃,b₄

proof end;

Lemma7: for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st len b₃ <= b₁ holds
b₃ | b₁ = b₃

proof end;

Lemma8: for b₁ being Function
for b₂ being set st not b₂ in rng b₁ holds
b₁ " {b₂} = {}

proof end;

theorem Th8: :: RFUNCT_3:8

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being real number st b₃ <> 0 holds
b₂ " {(b₄ / b₃)} = (b₃ (#) b₂) " {b₄}

proof end;

theorem Th9: :: RFUNCT_3:9

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds (0 (#) b₂) " {0} = dom b₂

proof end;

theorem Th10: :: RFUNCT_3:10

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real st 0 < b₃ holds
(abs b₂) " {b₃} = b₂ " {(- b₃),b₃}

proof end;

theorem Th11: :: RFUNCT_3:11

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds (abs b₂) " {0} = b₂ " {0}

proof end;

theorem Th12: :: RFUNCT_3:12

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real st b₃ < 0 holds
(abs b₂) " {b₃} = {}

proof end;

theorem Th13: :: RFUNCT_3:13

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL
for b₄ being PartFunc of b₂, REAL
for b₅ being Real st b₅ <> 0 holds
( b₃,b₄ are_fiberwise_equipotent iff b₅ (#) b₃,b₅ (#) b₄ are_fiberwise_equipotent )

proof end;

theorem Th14: :: RFUNCT_3:14

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL
for b₄ being PartFunc of b₂, REAL holds
( b₃,b₄ are_fiberwise_equipotent iff - b₃, - b₄ are_fiberwise_equipotent )

proof end;

theorem Th15: :: RFUNCT_3:15

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL
for b₄ being PartFunc of b₂, REAL st b₃,b₄ are_fiberwise_equipotent holds
abs b₃, abs b₄ are_fiberwise_equipotent

proof end;

definition

let c₁, c₂ be set ;
mode PartFunc-set of c₁,c₂ -> set means :Def3: :: RFUNCT_3:def 3
for b₁ being Element of a₃ holds b₁ is PartFunc of a₁,a₂;
existence

proof end;

end;

:: deftheorem Def3 defines PartFunc-set RFUNCT_3:def 3 :

registration

let c₁, c₂ be set ;
cluster non empty PartFunc-set of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
mode PFUNC_DOMAIN of a₁,a₂ is non empty PartFunc-set of a₁,a₂;

end;

definition

let c₁, c₂ be set ;
redefine func PFuncs as PFuncs c₁,c₂ -> PartFunc-set of a₁,a₂;
coherence

proof end;

let c₃ be non empty PartFunc-set of c₁,c₂;
redefine mode Element as Element of c₃ -> PartFunc of a₁,a₂;
coherence by Def3;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Subset of c₁;
let c₄ be Element of c₂;
redefine func --> as c₃ --> c₄ -> Element of PFuncs a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be real-membered set ;
let c₃, c₄ be Element of PFuncs c₁,c₂;
redefine func + as c₃ + c₄ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

redefine func - as c₃ - c₄ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

redefine func (#) as c₃ (#) c₄ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

redefine func / as c₃ / c₄ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be real-membered set ;
let c₃ be Element of PFuncs c₁,c₂;
redefine func abs as abs c₃ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

redefine func - as - c₃ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

redefine func ^ as c₃ ^ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be real-membered set ;
let c₃ be Element of PFuncs c₁,c₂;
let c₄ be real number ;
redefine func (#) as c₄ (#) c₃ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
func addpfunc c₁ -> BinOp of PFuncs a₁,REAL means :Def4: :: RFUNCT_3:def 4
for b₁, b₂ being Element of PFuncs a₁,REAL holds a₂ . b₁,b₂ = b₁ + b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines addpfunc RFUNCT_3:def 4 :

theorem Th16: :: RFUNCT_3:16

for b₁ being non empty set holds addpfunc b₁ is commutative

proof end;

theorem Th17: :: RFUNCT_3:17

for b₁ being non empty set holds addpfunc b₁ is associative

proof end;

theorem Th18: :: RFUNCT_3:18

for b₁ being non empty set holds ([#] b₁) --> 0 is_a_unity_wrt addpfunc b₁

proof end;

theorem Th19: :: RFUNCT_3:19

for b₁ being non empty set holds the_unity_wrt (addpfunc b₁) = ([#] b₁) --> 0

proof end;

theorem Th20: :: RFUNCT_3:20

for b₁ being non empty set holds addpfunc b₁ has_a_unity

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of PFuncs c₁,REAL ;
func Sum c₂ -> Element of PFuncs a₁,REAL equals :: RFUNCT_3:def 5
(addpfunc a₁) $$ a₂;
correctness ;

end;

:: deftheorem Def5 defines Sum RFUNCT_3:def 5 :

theorem Th21: :: RFUNCT_3:21

for b₁ being non empty set holds Sum (<*> (PFuncs b₁,REAL )) = ([#] b₁) --> 0

proof end;

theorem Th22: :: RFUNCT_3:22

for b₁ being non empty set
for b₂ being Element of PFuncs b₁,REAL holds Sum <*b₂*> = b₂ by FINSOP_1:12;

theorem Th23: :: RFUNCT_3:23

for b₁ being non empty set
for b₂ being FinSequence of PFuncs b₁,REAL
for b₃ being Element of PFuncs b₁,REAL holds Sum (b₂ ^ <*b₃*>) = (Sum b₂) + b₃

proof end;

theorem Th24: :: RFUNCT_3:24

for b₁ being non empty set
for b₂, b₃ being FinSequence of PFuncs b₁,REAL holds Sum (b₂ ^ b₃) = (Sum b₂) + (Sum b₃)

proof end;

theorem Th25: :: RFUNCT_3:25

for b₁ being non empty set
for b₂ being FinSequence of PFuncs b₁,REAL
for b₃ being Element of PFuncs b₁,REAL holds Sum (<*b₃*> ^ b₂) = b₃ + (Sum b₂)

proof end;

theorem Th26: :: RFUNCT_3:26

for b₁ being non empty set
for b₂, b₃ being Element of PFuncs b₁,REAL holds Sum <*b₂,b₃*> = b₂ + b₃

proof end;

theorem Th27: :: RFUNCT_3:27

for b₁ being non empty set
for b₂, b₃, b₄ being Element of PFuncs b₁,REAL holds Sum <*b₂,b₃,b₄*> = (b₂ + b₃) + b₄

proof end;

theorem Th28: :: RFUNCT_3:28

for b₁ being non empty set
for b₂, b₃ being FinSequence of PFuncs b₁,REAL st b₂,b₃ are_fiberwise_equipotent holds
Sum b₂ = Sum b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence;
func CHI c₂,c₁ -> FinSequence of PFuncs a₁,REAL means :Def6: :: RFUNCT_3:def 6
( len a₃ = len a₂ & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ = chi (a₂ . b₁),a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines CHI RFUNCT_3:def 6 :

definition

let c₁ be non empty set ;
let c₂ be FinSequence of PFuncs c₁,REAL ;
let c₃ be FinSequence of REAL ;
func c₃ (#) c₂ -> FinSequence of PFuncs a₁,REAL means :Def7: :: RFUNCT_3:def 7
( len a₄ = min (len a₃),(len a₂) & ( for b₁ being Nat st b₁ in dom a₄ holds
for b₂ being PartFunc of a₁, REAL
for b₃ being Real st b₃ = a₃ . b₁ & b₂ = a₂ . b₁ holds
a₄ . b₁ = b₃ (#) b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines (#) RFUNCT_3:def 7 :

definition

let c₁ be non empty set ;
let c₂ be FinSequence of PFuncs c₁,REAL ;
let c₃ be Element of c₁;
func c₂ # c₃ -> FinSequence of REAL means :Def8: :: RFUNCT_3:def 8
( len a₄ = len a₂ & ( for b₁ being Nat
for b₂ being Element of PFuncs a₁,REAL st b₁ in dom a₄ & a₂ . b₁ = b₂ holds
a₄ . b₁ = b₂ . a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines # RFUNCT_3:def 8 :

definition

let c₁, c₂ be non empty set ;
let c₃ be FinSequence of PFuncs c₁,c₂;
let c₄ be Element of c₁;
pred c₄ is_common_for_dom c₃ means :Def9: :: RFUNCT_3:def 9
for b₁ being Element of PFuncs a₁,a₂
for b₂ being Nat st b₂ in dom a₃ & a₃ . b₂ = b₁ holds
a₄ in dom b₁;

end;

:: deftheorem Def9 defines is_common_for_dom RFUNCT_3:def 9 :

theorem Th29: :: RFUNCT_3:29

for b₁, b₂ being non empty set
for b₃ being FinSequence of PFuncs b₁,b₂
for b₄ being Element of b₁
for b₅ being Nat st b₄ is_common_for_dom b₃ & b₅ <> 0 holds
b₄ is_common_for_dom b₃ | b₅

proof end;

theorem Th30: :: RFUNCT_3:30

for b₁, b₂ being non empty set
for b₃ being FinSequence of PFuncs b₁,b₂
for b₄ being Element of b₁
for b₅ being Nat st b₄ is_common_for_dom b₃ holds
b₄ is_common_for_dom b₃ /^ b₅

proof end;

theorem Th31: :: RFUNCT_3:31

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of PFuncs b₁,REAL st len b₃ <> 0 holds
( b₂ is_common_for_dom b₃ iff b₂ in dom (Sum b₃) )

proof end;

theorem Th32: :: RFUNCT_3:32

for b₁ being non empty set
for b₂ being FinSequence of PFuncs b₁,REAL
for b₃ being Element of b₁
for b₄ being Nat holds (b₂ | b₄) # b₃ = (b₂ # b₃) | b₄

proof end;

theorem Th33: :: RFUNCT_3:33

for b₁ being non empty set
for b₂ being FinSequence
for b₃ being Element of b₁ holds b₃ is_common_for_dom CHI b₂,b₁

proof end;

theorem Th34: :: RFUNCT_3:34

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of PFuncs b₁,REAL
for b₄ being FinSequence of REAL st b₂ is_common_for_dom b₃ holds
b₂ is_common_for_dom b₄ (#) b₃

proof end;

theorem Th35: :: RFUNCT_3:35

for b₁ being non empty set
for b₂ being FinSequence
for b₃ being FinSequence of REAL
for b₄ being Element of b₁ holds b₄ is_common_for_dom b₃ (#) (CHI b₂,b₁)

proof end;

theorem Th36: :: RFUNCT_3:36

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of PFuncs b₁,REAL st b₂ is_common_for_dom b₃ holds
(Sum b₃) . b₂ = Sum (b₃ # b₂)

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, REAL ;
func max+ c₂ -> PartFunc of a₁, REAL means :Def10: :: RFUNCT_3:def 10
( dom a₃ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₃ holds
a₃ . b₁ = max+ (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func max- c₂ -> PartFunc of a₁, REAL means :Def11: :: RFUNCT_3:def 11
( dom a₃ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₃ holds
a₃ . b₁ = max- (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines max+ RFUNCT_3:def 10 :

:: deftheorem Def11 defines max- RFUNCT_3:def 11 :

theorem Th37: :: RFUNCT_3:37

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds
( b₂ = (max+ b₂) - (max- b₂) & abs b₂ = (max+ b₂) + (max- b₂) & 2 (#) (max+ b₂) = b₂ + (abs b₂) )

proof end;

theorem Th38: :: RFUNCT_3:38

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real st 0 < b₃ holds
b₂ " {b₃} = (max+ b₂) " {b₃}

proof end;

theorem Th39: :: RFUNCT_3:39

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds b₂ " (left_closed_halfline 0) = (max+ b₂) " {0}

proof end;

theorem Th40: :: RFUNCT_3:40

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
0 <= (max+ b₂) . b₃

proof end;

theorem Th41: :: RFUNCT_3:41

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real st 0 < b₃ holds
b₂ " {(- b₃)} = (max- b₂) " {b₃}

proof end;

theorem Th42: :: RFUNCT_3:42

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds b₂ " (right_closed_halfline 0) = (max- b₂) " {0}

proof end;

theorem Th43: :: RFUNCT_3:43

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
0 <= (max- b₂) . b₃

proof end;

theorem Th44: :: RFUNCT_3:44

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL
for b₄ being PartFunc of b₂, REAL st b₃,b₄ are_fiberwise_equipotent holds
max+ b₃, max+ b₄ are_fiberwise_equipotent

proof end;

theorem Th45: :: RFUNCT_3:45

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL
for b₄ being PartFunc of b₂, REAL st b₃,b₄ are_fiberwise_equipotent holds
max- b₃, max- b₄ are_fiberwise_equipotent

proof end;

registration

let c₁, c₂ be set ;
cluster finite Relation of a₁,a₂;
existence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be finite PartFunc of c₁, REAL ;
cluster max+ a₂ -> finite ;
coherence

proof end;

cluster max- a₂ -> finite ;
coherence

proof end;

end;

theorem Th46: :: RFUNCT_3:46

for b₁, b₂ being non empty set
for b₃ being finite PartFunc of b₁, REAL
for b₄ being finite PartFunc of b₂, REAL st max+ b₃, max+ b₄ are_fiberwise_equipotent & max- b₃, max- b₄ are_fiberwise_equipotent holds
b₃,b₄ are_fiberwise_equipotent

proof end;

theorem Th47: :: RFUNCT_3:47

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set holds (max+ b₂) | b₃ = max+ (b₂ | b₃)

proof end;

theorem Th48: :: RFUNCT_3:48

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set holds (max- b₂) | b₃ = max- (b₂ | b₃)

proof end;

theorem Th49: :: RFUNCT_3:49

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st ( for b₃ being Element of b₁ st b₃ in dom b₂ holds
b₂ . b₃ >= 0 ) holds
max+ b₂ = b₂

proof end;

theorem Th50: :: RFUNCT_3:50

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st ( for b₃ being Element of b₁ st b₃ in dom b₂ holds
b₂ . b₃ <= 0 ) holds
max- b₂ = - b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be Real;
func c₂ - c₃ -> PartFunc of a₁, REAL means :Def12: :: RFUNCT_3:def 12
( dom a₄ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = (a₂ . b₁) - a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines - RFUNCT_3:def 12 :

theorem Th51: :: RFUNCT_3:51

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds b₂ - 0 = b₂

proof end;

theorem Th52: :: RFUNCT_3:52

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real
for b₄ being set holds (b₂ | b₄) - b₃ = (b₂ - b₃) | b₄

proof end;

theorem Th53: :: RFUNCT_3:53

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being Real holds b₂ " {(b₄ + b₃)} = (b₂ - b₃) " {b₄}

proof end;

theorem Th54: :: RFUNCT_3:54

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL
for b₄ being PartFunc of b₂, REAL
for b₅ being Real holds
( b₃,b₄ are_fiberwise_equipotent iff b₃ - b₅,b₄ - b₅ are_fiberwise_equipotent )

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be set ;
pred c₁ is_convex_on c₂ means :Def13: :: RFUNCT_3:def 13
( a₂ c= dom a₁ & ( for b₁ being Real st 0 <= b₁ & b₁ <= 1 holds
for b₂, b₃ being Real st b₂ in a₂ & b₃ in a₂ & (b₁ * b₂) + ((1 - b₁) * b₃) in a₂ holds
a₁ . ((b₁ * b₂) + ((1 - b₁) * b₃)) <= (b₁ * (a₁ . b₂)) + ((1 - b₁) * (a₁ . b₃)) ) );

end;

:: deftheorem Def13 defines is_convex_on RFUNCT_3:def 13 :

theorem Th55: :: RFUNCT_3:55

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL holds
( b₃ is_convex_on [.b₁,b₂.] iff ( [.b₁,b₂.] c= dom b₃ & ( for b₄ being Real st 0 <= b₄ & b₄ <= 1 holds
for b₅, b₆ being Real st b₅ in [.b₁,b₂.] & b₆ in [.b₁,b₂.] holds
b₃ . ((b₄ * b₅) + ((1 - b₄) * b₆)) <= (b₄ * (b₃ . b₅)) + ((1 - b₄) * (b₃ . b₆)) ) ) )

proof end;

theorem Th56: :: RFUNCT_3:56

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL holds
( b₃ is_convex_on [.b₁,b₂.] iff ( [.b₁,b₂.] c= dom b₃ & ( for b₄, b₅, b₆ being Real st b₄ in [.b₁,b₂.] & b₅ in [.b₁,b₂.] & b₆ in [.b₁,b₂.] & b₄ < b₅ & b₅ < b₆ holds
((b₃ . b₄) - (b₃ . b₅)) / (b₄ - b₅) <= ((b₃ . b₅) - (b₃ . b₆)) / (b₅ - b₆) ) ) )

proof end;

theorem Th57: :: RFUNCT_3:57

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being set st b₁ is_convex_on b₂ & b₃ c= b₂ holds
b₁ is_convex_on b₃

proof end;

theorem Th58: :: RFUNCT_3:58

for b₁ being PartFunc of REAL , REAL
for b₂ being set
for b₃ being Real holds
( b₁ is_convex_on b₂ iff b₁ - b₃ is_convex_on b₂ )

proof end;

theorem Th59: :: RFUNCT_3:59

for b₁ being PartFunc of REAL , REAL
for b₂ being set
for b₃ being Real st 0 < b₃ holds
( b₁ is_convex_on b₂ iff b₃ (#) b₁ is_convex_on b₂ )

proof end;

theorem Th60: :: RFUNCT_3:60

for b₁ being PartFunc of REAL , REAL
for b₂ being set st b₂ c= dom b₁ holds
0 (#) b₁ is_convex_on b₂

proof end;

theorem Th61: :: RFUNCT_3:61

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being set st b₁ is_convex_on b₃ & b₂ is_convex_on b₃ holds
b₁ + b₂ is_convex_on b₃

proof end;

theorem Th62: :: RFUNCT_3:62

for b₁ being PartFunc of REAL , REAL
for b₂ being set
for b₃ being Real st b₁ is_convex_on b₂ holds
max+ (b₁ - b₃) is_convex_on b₂

proof end;

theorem Th63: :: RFUNCT_3:63

for b₁ being PartFunc of REAL , REAL
for b₂ being set st b₁ is_convex_on b₂ holds
max+ b₁ is_convex_on b₂

proof end;

theorem Th64: :: RFUNCT_3:64

id ([#] REAL ) is_convex_on REAL

proof end;

theorem Th65: :: RFUNCT_3:65

for b₁ being Real holds max+ ((id ([#] REAL )) - b₁) is_convex_on REAL by Th62, Th64;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be set ;
assume E53: dom (c₂ | c₃) is finite ;
func FinS c₂,c₃ -> non-increasing FinSequence of REAL means :Def14: :: RFUNCT_3:def 14
a₂ | a₃,a₄ are_fiberwise_equipotent ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines FinS RFUNCT_3:def 14 :

theorem Th66: :: RFUNCT_3:66

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set st dom (b₂ | b₃) is finite holds
FinS b₂,(dom (b₂ | b₃)) = FinS b₂,b₃

proof end;

theorem Th67: :: RFUNCT_3:67

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set st dom (b₂ | b₃) is finite holds
FinS (b₂ | b₃),b₃ = FinS b₂,b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be finite set ;
redefine func | as c₂ | c₃ -> finite PartFunc of a₁, REAL ;
coherence

proof end;

end;

theorem Th68: :: RFUNCT_3:68

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being set
for b₄ being PartFunc of b₁, REAL st b₃ is finite & b₂ in dom (b₄ | b₃) holds
(FinS b₄,(b₃ \ {b₂})) ^ <*(b₄ . b₂)*>,b₄ | b₃ are_fiberwise_equipotent

proof end;

theorem Th69: :: RFUNCT_3:69

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being set
for b₄ being PartFunc of b₁, REAL st dom (b₄ | b₃) is finite & b₂ in dom (b₄ | b₃) holds
(FinS b₄,(b₃ \ {b₂})) ^ <*(b₄ . b₂)*>,b₄ | b₃ are_fiberwise_equipotent

proof end;

theorem Th70: :: RFUNCT_3:70

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set
for b₄ being finite set st b₄ = dom (b₂ | b₃) holds
len (FinS b₂,b₃) = card b₄

proof end;

theorem Th71: :: RFUNCT_3:71

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds FinS b₂,{} = <*> REAL

proof end;

theorem Th72: :: RFUNCT_3:72

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
FinS b₂,{b₃} = <*(b₂ . b₃)*>

proof end;

theorem Th73: :: RFUNCT_3:73

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set
for b₄ being Element of b₁ st dom (b₂ | b₃) is finite & b₄ in dom (b₂ | b₃) & (FinS b₂,b₃) . (len (FinS b₂,b₃)) = b₂ . b₄ holds
FinS b₂,b₃ = (FinS b₂,(b₃ \ {b₄})) ^ <*(b₂ . b₄)*>

proof end;

defpred S₁[ Nat] means for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being set
for b₅ being finite set st b₅ = dom (b₂ | b₄) & dom (b₂ | b₃) is finite & b₄ c= b₃ & a₁ = card b₅ & ( for b₆, b₇ being Element of b₁ st b₆ in dom (b₂ | b₄) & b₇ in dom (b₂ | (b₃ \ b₄)) holds
b₂ . b₆ >= b₂ . b₇ ) holds
FinS b₂,b₃ = (FinS b₂,b₄) ^ (FinS b₂,(b₃ \ b₄));

Lemma62: S₁[0]

proof end;

Lemma63: for b₁ being Nat st S₁[b₁] holds
S₁[b₁ + 1]

proof end;

theorem Th74: :: RFUNCT_3:74

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being set st dom (b₂ | b₃) is finite & b₄ c= b₃ & ( for b₅, b₆ being Element of b₁ st b₅ in dom (b₂ | b₄) & b₆ in dom (b₂ | (b₃ \ b₄)) holds
b₂ . b₅ >= b₂ . b₆ ) holds
FinS b₂,b₃ = (FinS b₂,b₄) ^ (FinS b₂,(b₃ \ b₄))

proof end;

theorem Th75: :: RFUNCT_3:75

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real
for b₄ being set
for b₅ being Element of b₁ st dom (b₂ | b₄) is finite & b₅ in dom (b₂ | b₄) holds
( (FinS (b₂ - b₃),b₄) . (len (FinS (b₂ - b₃),b₄)) = (b₂ - b₃) . b₅ iff (FinS b₂,b₄) . (len (FinS b₂,b₄)) = b₂ . b₅ )

proof end;

theorem Th76: :: RFUNCT_3:76

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Real
for b₄ being set
for b₅ being finite set st b₅ = dom (b₂ | b₄) holds
FinS (b₂ - b₃),b₄ = (FinS b₂,b₄) - ((card b₅) |-> b₃)

proof end;

theorem Th77: :: RFUNCT_3:77

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set st dom (b₂ | b₃) is finite & ( for b₄ being Element of b₁ st b₄ in dom (b₂ | b₃) holds
b₂ . b₄ >= 0 ) holds
FinS (max+ b₂),b₃ = FinS b₂,b₃

proof end;

theorem Th78: :: RFUNCT_3:78

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set
for b₄ being Real
for b₅ being finite set st b₅ = dom (b₂ | b₃) & rng (b₂ | b₃) = {b₄} holds
FinS b₂,b₃ = (card b₅) |-> b₄

proof end;

theorem Th79: :: RFUNCT_3:79

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being set st dom (b₂ | (b₃ \/ b₄)) is finite & b₃ misses b₄ holds
FinS b₂,(b₃ \/ b₄),(FinS b₂,b₃) ^ (FinS b₂,b₄) are_fiberwise_equipotent

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be set ;
func Sum c₂,c₃ -> Real equals :: RFUNCT_3:def 15
Sum (FinS a₂,a₃);
correctness ;

end;

:: deftheorem Def15 defines Sum RFUNCT_3:def 15 :

theorem Th80: :: RFUNCT_3:80

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set
for b₄ being Real st dom (b₂ | b₃) is finite holds
Sum (b₄ (#) b₂),b₃ = b₄ * (Sum b₂,b₃)

proof end;

theorem Th81: :: RFUNCT_3:81

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, REAL
for b₄ being set
for b₅ being finite set st b₅ = dom (b₂ | b₄) & dom (b₂ | b₄) = dom (b₃ | b₄) holds
Sum (b₂ + b₃),b₄ = (Sum b₂,b₄) + (Sum b₃,b₄)

proof end;

theorem Th82: :: RFUNCT_3:82

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, REAL
for b₄ being set st dom (b₂ | b₄) is finite & dom (b₂ | b₄) = dom (b₃ | b₄) holds
Sum (b₂ - b₃),b₄ = (Sum b₂,b₄) - (Sum b₃,b₄)

proof end;

theorem Th83: :: RFUNCT_3:83

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being set
for b₄ being Real
for b₅ being finite set st b₅ = dom (b₂ | b₃) holds
Sum (b₂ - b₄),b₃ = (Sum b₂,b₃) - (b₄ * (card b₅))

proof end;

theorem Th84: :: RFUNCT_3:84

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds Sum b₂,{} = 0 by Th71, RVSUM_1:102;

theorem Th85: :: RFUNCT_3:85

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of b₁ st b₃ in dom b₂ holds
Sum b₂,{b₃} = b₂ . b₃

proof end;

theorem Th86: :: RFUNCT_3:86

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being set st dom (b₂ | (b₃ \/ b₄)) is finite & b₃ misses b₄ holds
Sum b₂,(b₃ \/ b₄) = (Sum b₂,b₃) + (Sum b₂,b₄)

proof end;

theorem Th87: :: RFUNCT_3:87

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being set st dom (b₂ | (b₃ \/ b₄)) is finite & dom (b₂ | b₃) misses dom (b₂ | b₄) holds
Sum b₂,(b₃ \/ b₄) = (Sum b₂,b₃) + (Sum b₂,b₄)

proof end;