:: by Jaros{\l}aw Kotowicz and Yuji Sakai

::

:: Received March 15, 1993

:: Copyright (c) 1993-2012 Association of Mizar Users

begin

definition

let r be real number ;

correctness

coherence

max (r,0) is Real;

by XREAL_0:def 1;

correctness

coherence

max ((- r),0) is Real;

by XREAL_0:def 1;

end;
correctness

coherence

max (r,0) is Real;

by XREAL_0:def 1;

correctness

coherence

max ((- r),0) is Real;

by XREAL_0:def 1;

Lm1: for n being Element of NAT

for D being non empty set

for f being FinSequence of D st len f <= n holds

f | n = f

proof end;

Lm2: for f being Function

for x being set st not x in rng f holds

f " {x} = {}

proof end;

begin

theorem Th6: :: RFUNCT_3:6

for D being non empty set

for F being PartFunc of D,REAL

for r, s being real number st r <> 0 holds

F " {(s / r)} = (r (#) F) " {s}

for F being PartFunc of D,REAL

for r, s being real number st r <> 0 holds

F " {(s / r)} = (r (#) F) " {s}

proof end;

theorem Th8: :: RFUNCT_3:8

for D being non empty set

for F being PartFunc of D,REAL

for r being Real st 0 < r holds

(abs F) " {r} = F " {(- r),r}

for F being PartFunc of D,REAL

for r being Real st 0 < r holds

(abs F) " {r} = F " {(- r),r}

proof end;

theorem Th10: :: RFUNCT_3:10

for D being non empty set

for F being PartFunc of D,REAL

for r being Real st r < 0 holds

(abs F) " {r} = {}

for F being PartFunc of D,REAL

for r being Real st r < 0 holds

(abs F) " {r} = {}

proof end;

theorem Th11: :: RFUNCT_3:11

for D, C being non empty set

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL

for r being Real st r <> 0 holds

( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL

for r being Real st r <> 0 holds

( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )

proof end;

theorem :: RFUNCT_3:12

for D, C being non empty set

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL holds

( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL holds

( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )

proof end;

theorem :: RFUNCT_3:13

for D, C being non empty set

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds

abs F, abs G are_fiberwise_equipotent

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds

abs F, abs G are_fiberwise_equipotent

proof end;

definition

let X, Y be set ;

ex b_{1} being set st

for x being Element of b_{1} holds x is PartFunc of X,Y

end;
mode PartFunc-set of X,Y -> set means :Def3: :: RFUNCT_3:def 3

for x being Element of it holds x is PartFunc of X,Y;

existence for x being Element of it holds x is PartFunc of X,Y;

ex b

for x being Element of b

proof end;

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

for X, Y being set

for b_{3} being set holds

( b_{3} is PartFunc-set of X,Y iff for x being Element of b_{3} holds x is PartFunc of X,Y );

for X, Y being set

for b

( b

registration
end;

definition

let X, Y be set ;

:: original: PFuncs

redefine func PFuncs (X,Y) -> PartFunc-set of X,Y;

coherence

PFuncs (X,Y) is PartFunc-set of X,Y

:: original: Element

redefine mode Element of P -> PartFunc of X,Y;

coherence

for b_{1} being Element of P holds b_{1} is PartFunc of X,Y
by Def3;

end;
:: original: PFuncs

redefine func PFuncs (X,Y) -> PartFunc-set of X,Y;

coherence

PFuncs (X,Y) is PartFunc-set of X,Y

proof end;

let P be non empty PartFunc-set of X,Y;:: original: Element

redefine mode Element of P -> PartFunc of X,Y;

coherence

for b

definition

let D, C be non empty set ;

let X be Subset of D;

let c be Element of C;

:: original: -->

redefine func X --> c -> Element of PFuncs (D,C);

coherence

X --> c is Element of PFuncs (D,C)

end;
let X be Subset of D;

let c be Element of C;

:: original: -->

redefine func X --> c -> Element of PFuncs (D,C);

coherence

X --> c is Element of PFuncs (D,C)

proof end;

:: awaryjne, A.T.

registration

let D be non empty set ;

let E be real-membered set ;

coherence

for b_{1} being Element of PFuncs (D,E) holds b_{1} is real-valued
;

end;
let E be real-membered set ;

coherence

for b

definition

let D be non empty set ;

let E be real-membered set ;

let F1, F2 be Element of PFuncs (D,E);

:: original: +

redefine func F1 + F2 -> Element of PFuncs (D,REAL);

coherence

F1 + F2 is Element of PFuncs (D,REAL)

redefine func F1 - F2 -> Element of PFuncs (D,REAL);

coherence

F1 - F2 is Element of PFuncs (D,REAL)

redefine func F1 (#) F2 -> Element of PFuncs (D,REAL);

coherence

F1 (#) F2 is Element of PFuncs (D,REAL)

redefine func F1 / F2 -> Element of PFuncs (D,REAL);

coherence

F1 / F2 is Element of PFuncs (D,REAL)

end;
let E be real-membered set ;

let F1, F2 be Element of PFuncs (D,E);

:: original: +

redefine func F1 + F2 -> Element of PFuncs (D,REAL);

coherence

F1 + F2 is Element of PFuncs (D,REAL)

proof end;

:: original: -redefine func F1 - F2 -> Element of PFuncs (D,REAL);

coherence

F1 - F2 is Element of PFuncs (D,REAL)

proof end;

:: original: (#)redefine func F1 (#) F2 -> Element of PFuncs (D,REAL);

coherence

F1 (#) F2 is Element of PFuncs (D,REAL)

proof end;

:: original: /redefine func F1 / F2 -> Element of PFuncs (D,REAL);

coherence

F1 / F2 is Element of PFuncs (D,REAL)

proof end;

definition

let D be non empty set ;

let E be real-membered set ;

let F be Element of PFuncs (D,E);

:: original: |.

redefine func abs F -> Element of PFuncs (D,REAL);

coherence

|.F.| is Element of PFuncs (D,REAL)

redefine func - F -> Element of PFuncs (D,REAL);

coherence

- F is Element of PFuncs (D,REAL)

redefine func F ^ -> Element of PFuncs (D,REAL);

coherence

F ^ is Element of PFuncs (D,REAL)

end;
let E be real-membered set ;

let F be Element of PFuncs (D,E);

:: original: |.

redefine func abs F -> Element of PFuncs (D,REAL);

coherence

|.F.| is Element of PFuncs (D,REAL)

proof end;

:: original: -redefine func - F -> Element of PFuncs (D,REAL);

coherence

- F is Element of PFuncs (D,REAL)

proof end;

:: original: ^redefine func F ^ -> Element of PFuncs (D,REAL);

coherence

F ^ is Element of PFuncs (D,REAL)

proof end;

definition

let D be non empty set ;

let E be real-membered set ;

let F be Element of PFuncs (D,E);

let r be real number ;

:: original: (#)

redefine func r (#) F -> Element of PFuncs (D,REAL);

coherence

r (#) F is Element of PFuncs (D,REAL)

end;
let E be real-membered set ;

let F be Element of PFuncs (D,E);

let r be real number ;

:: original: (#)

redefine func r (#) F -> Element of PFuncs (D,REAL);

coherence

r (#) F is Element of PFuncs (D,REAL)

proof end;

definition

let D be non empty set ;

ex b_{1} being BinOp of (PFuncs (D,REAL)) st

for F1, F2 being Element of PFuncs (D,REAL) holds b_{1} . (F1,F2) = F1 + F2

for b_{1}, b_{2} being BinOp of (PFuncs (D,REAL)) st ( for F1, F2 being Element of PFuncs (D,REAL) holds b_{1} . (F1,F2) = F1 + F2 ) & ( for F1, F2 being Element of PFuncs (D,REAL) holds b_{2} . (F1,F2) = F1 + F2 ) holds

b_{1} = b_{2}

end;
func addpfunc D -> BinOp of (PFuncs (D,REAL)) means :Def4: :: RFUNCT_3:def 4

for F1, F2 being Element of PFuncs (D,REAL) holds it . (F1,F2) = F1 + F2;

existence for F1, F2 being Element of PFuncs (D,REAL) holds it . (F1,F2) = F1 + F2;

ex b

for F1, F2 being Element of PFuncs (D,REAL) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines addpfunc RFUNCT_3:def 4 :

for D being non empty set

for b_{2} being BinOp of (PFuncs (D,REAL)) holds

( b_{2} = addpfunc D iff for F1, F2 being Element of PFuncs (D,REAL) holds b_{2} . (F1,F2) = F1 + F2 );

for D being non empty set

for b

( b

definition

let D be non empty set ;

let f be FinSequence of PFuncs (D,REAL);

correctness

coherence

(addpfunc D) $$ f is Element of PFuncs (D,REAL);

;

end;
let f be FinSequence of PFuncs (D,REAL);

correctness

coherence

(addpfunc D) $$ f is Element of PFuncs (D,REAL);

;

:: deftheorem defines Sum RFUNCT_3:def 5 :

for D being non empty set

for f being FinSequence of PFuncs (D,REAL) holds Sum f = (addpfunc D) $$ f;

for D being non empty set

for f being FinSequence of PFuncs (D,REAL) holds Sum f = (addpfunc D) $$ f;

theorem Th20: :: RFUNCT_3:20

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for G being Element of PFuncs (D,REAL) holds Sum (f ^ <*G*>) = (Sum f) + G

for f being FinSequence of PFuncs (D,REAL)

for G being Element of PFuncs (D,REAL) holds Sum (f ^ <*G*>) = (Sum f) + G

proof end;

theorem Th21: :: RFUNCT_3:21

for D being non empty set

for f1, f2 being FinSequence of PFuncs (D,REAL) holds Sum (f1 ^ f2) = (Sum f1) + (Sum f2)

for f1, f2 being FinSequence of PFuncs (D,REAL) holds Sum (f1 ^ f2) = (Sum f1) + (Sum f2)

proof end;

theorem :: RFUNCT_3:22

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for G being Element of PFuncs (D,REAL) holds Sum (<*G*> ^ f) = G + (Sum f)

for f being FinSequence of PFuncs (D,REAL)

for G being Element of PFuncs (D,REAL) holds Sum (<*G*> ^ f) = G + (Sum f)

proof end;

theorem :: RFUNCT_3:24

for D being non empty set

for G1, G2, G3 being Element of PFuncs (D,REAL) holds Sum <*G1,G2,G3*> = (G1 + G2) + G3

for G1, G2, G3 being Element of PFuncs (D,REAL) holds Sum <*G1,G2,G3*> = (G1 + G2) + G3

proof end;

theorem :: RFUNCT_3:25

for D being non empty set

for f, g being FinSequence of PFuncs (D,REAL) st f,g are_fiberwise_equipotent holds

Sum f = Sum g

for f, g being FinSequence of PFuncs (D,REAL) st f,g are_fiberwise_equipotent holds

Sum f = Sum g

proof end;

definition

let D be non empty set ;

let f be FinSequence;

ex b_{1} being FinSequence of PFuncs (D,REAL) st

( len b_{1} = len f & ( for n being Element of NAT st n in dom b_{1} holds

b_{1} . n = chi ((f . n),D) ) )

for b_{1}, b_{2} being FinSequence of PFuncs (D,REAL) st len b_{1} = len f & ( for n being Element of NAT st n in dom b_{1} holds

b_{1} . n = chi ((f . n),D) ) & len b_{2} = len f & ( for n being Element of NAT st n in dom b_{2} holds

b_{2} . n = chi ((f . n),D) ) holds

b_{1} = b_{2}

end;
let f be FinSequence;

func CHI (f,D) -> FinSequence of PFuncs (D,REAL) means :Def6: :: RFUNCT_3:def 6

( len it = len f & ( for n being Element of NAT st n in dom it holds

it . n = chi ((f . n),D) ) );

existence ( len it = len f & ( for n being Element of NAT st n in dom it holds

it . n = chi ((f . n),D) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines CHI RFUNCT_3:def 6 :

for D being non empty set

for f being FinSequence

for b_{3} being FinSequence of PFuncs (D,REAL) holds

( b_{3} = CHI (f,D) iff ( len b_{3} = len f & ( for n being Element of NAT st n in dom b_{3} holds

b_{3} . n = chi ((f . n),D) ) ) );

for D being non empty set

for f being FinSequence

for b

( b

b

definition

let D be non empty set ;

let f be FinSequence of PFuncs (D,REAL);

let R be FinSequence of REAL ;

ex b_{1} being FinSequence of PFuncs (D,REAL) st

( len b_{1} = min ((len R),(len f)) & ( for n being Element of NAT st n in dom b_{1} holds

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b_{1} . n = r (#) F ) )

for b_{1}, b_{2} being FinSequence of PFuncs (D,REAL) st len b_{1} = min ((len R),(len f)) & ( for n being Element of NAT st n in dom b_{1} holds

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b_{1} . n = r (#) F ) & len b_{2} = min ((len R),(len f)) & ( for n being Element of NAT st n in dom b_{2} holds

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b_{2} . n = r (#) F ) holds

b_{1} = b_{2}

end;
let f be FinSequence of PFuncs (D,REAL);

let R be FinSequence of REAL ;

func R (#) f -> FinSequence of PFuncs (D,REAL) means :Def7: :: RFUNCT_3:def 7

( len it = min ((len R),(len f)) & ( for n being Element of NAT st n in dom it holds

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

it . n = r (#) F ) );

existence ( len it = min ((len R),(len f)) & ( for n being Element of NAT st n in dom it holds

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

it . n = r (#) F ) );

ex b

( len b

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b

proof end;

uniqueness for b

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b

b

proof end;

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

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for R being FinSequence of REAL

for b_{4} being FinSequence of PFuncs (D,REAL) holds

( b_{4} = R (#) f iff ( len b_{4} = min ((len R),(len f)) & ( for n being Element of NAT st n in dom b_{4} holds

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b_{4} . n = r (#) F ) ) );

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for R being FinSequence of REAL

for b

( b

for F being PartFunc of D,REAL

for r being Real st r = R . n & F = f . n holds

b

definition

let D be non empty set ;

let f be FinSequence of PFuncs (D,REAL);

let d be Element of D;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len f & ( for n being Element of NAT st n in dom b_{1} holds

b_{1} . n = (f . n) . d ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len f & ( for n being Element of NAT st n in dom b_{1} holds

b_{1} . n = (f . n) . d ) & len b_{2} = len f & ( for n being Element of NAT st n in dom b_{2} holds

b_{2} . n = (f . n) . d ) holds

b_{1} = b_{2}

end;
let f be FinSequence of PFuncs (D,REAL);

let d be Element of D;

func f # d -> FinSequence of REAL means :Def8: :: RFUNCT_3:def 8

( len it = len f & ( for n being Element of NAT st n in dom it holds

it . n = (f . n) . d ) );

existence ( len it = len f & ( for n being Element of NAT st n in dom it holds

it . n = (f . n) . d ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines # RFUNCT_3:def 8 :

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for d being Element of D

for b_{4} being FinSequence of REAL holds

( b_{4} = f # d iff ( len b_{4} = len f & ( for n being Element of NAT st n in dom b_{4} holds

b_{4} . n = (f . n) . d ) ) );

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for d being Element of D

for b

( b

b

definition

let D, C be non empty set ;

let f be FinSequence of PFuncs (D,C);

let d be Element of D;

end;
let f be FinSequence of PFuncs (D,C);

let d be Element of D;

pred d is_common_for_dom f means :Def9: :: RFUNCT_3:def 9

for n being Element of NAT st n in dom f holds

d in dom (f . n);

for n being Element of NAT st n in dom f holds

d in dom (f . n);

:: deftheorem Def9 defines is_common_for_dom RFUNCT_3:def 9 :

for D, C being non empty set

for f being FinSequence of PFuncs (D,C)

for d being Element of D holds

( d is_common_for_dom f iff for n being Element of NAT st n in dom f holds

d in dom (f . n) );

for D, C being non empty set

for f being FinSequence of PFuncs (D,C)

for d being Element of D holds

( d is_common_for_dom f iff for n being Element of NAT st n in dom f holds

d in dom (f . n) );

theorem Th26: :: RFUNCT_3:26

for D, C being non empty set

for f being FinSequence of PFuncs (D,C)

for d being Element of D

for n being Element of NAT st d is_common_for_dom f & n <> 0 holds

d is_common_for_dom f | n

for f being FinSequence of PFuncs (D,C)

for d being Element of D

for n being Element of NAT st d is_common_for_dom f & n <> 0 holds

d is_common_for_dom f | n

proof end;

theorem :: RFUNCT_3:27

for D, C being non empty set

for f being FinSequence of PFuncs (D,C)

for d being Element of D

for n being Element of NAT st d is_common_for_dom f holds

d is_common_for_dom f /^ n

for f being FinSequence of PFuncs (D,C)

for d being Element of D

for n being Element of NAT st d is_common_for_dom f holds

d is_common_for_dom f /^ n

proof end;

theorem Th28: :: RFUNCT_3:28

for D being non empty set

for d being Element of D

for f being FinSequence of PFuncs (D,REAL) st len f <> 0 holds

( d is_common_for_dom f iff d in dom (Sum f) )

for d being Element of D

for f being FinSequence of PFuncs (D,REAL) st len f <> 0 holds

( d is_common_for_dom f iff d in dom (Sum f) )

proof end;

theorem Th29: :: RFUNCT_3:29

for D being non empty set

for f being FinSequence of PFuncs (D,REAL)

for d being Element of D

for n being Element of NAT holds (f | n) # d = (f # d) | n

for f being FinSequence of PFuncs (D,REAL)

for d being Element of D

for n being Element of NAT holds (f | n) # d = (f # d) | n

proof end;

theorem Th30: :: RFUNCT_3:30

for D being non empty set

for f being FinSequence

for d being Element of D holds d is_common_for_dom CHI (f,D)

for f being FinSequence

for d being Element of D holds d is_common_for_dom CHI (f,D)

proof end;

theorem Th31: :: RFUNCT_3:31

for D being non empty set

for d being Element of D

for f being FinSequence of PFuncs (D,REAL)

for R being FinSequence of REAL st d is_common_for_dom f holds

d is_common_for_dom R (#) f

for d being Element of D

for f being FinSequence of PFuncs (D,REAL)

for R being FinSequence of REAL st d is_common_for_dom f holds

d is_common_for_dom R (#) f

proof end;

theorem :: RFUNCT_3:32

for D being non empty set

for f being FinSequence

for R being FinSequence of REAL

for d being Element of D holds d is_common_for_dom R (#) (CHI (f,D)) by Th30, Th31;

for f being FinSequence

for R being FinSequence of REAL

for d being Element of D holds d is_common_for_dom R (#) (CHI (f,D)) by Th30, Th31;

theorem :: RFUNCT_3:33

for D being non empty set

for d being Element of D

for f being FinSequence of PFuncs (D,REAL) st d is_common_for_dom f holds

(Sum f) . d = Sum (f # d)

for d being Element of D

for f being FinSequence of PFuncs (D,REAL) st d is_common_for_dom f holds

(Sum f) . d = Sum (f # d)

proof end;

definition

let D be non empty set ;

let F be PartFunc of D,REAL;

ex b_{1} being PartFunc of D,REAL st

( dom b_{1} = dom F & ( for d being Element of D st d in dom b_{1} holds

b_{1} . d = max+ (F . d) ) )

for b_{1}, b_{2} being PartFunc of D,REAL st dom b_{1} = dom F & ( for d being Element of D st d in dom b_{1} holds

b_{1} . d = max+ (F . d) ) & dom b_{2} = dom F & ( for d being Element of D st d in dom b_{2} holds

b_{2} . d = max+ (F . d) ) holds

b_{1} = b_{2}

ex b_{1} being PartFunc of D,REAL st

( dom b_{1} = dom F & ( for d being Element of D st d in dom b_{1} holds

b_{1} . d = max- (F . d) ) )

for b_{1}, b_{2} being PartFunc of D,REAL st dom b_{1} = dom F & ( for d being Element of D st d in dom b_{1} holds

b_{1} . d = max- (F . d) ) & dom b_{2} = dom F & ( for d being Element of D st d in dom b_{2} holds

b_{2} . d = max- (F . d) ) holds

b_{1} = b_{2}

end;
let F be PartFunc of D,REAL;

func max+ F -> PartFunc of D,REAL means :Def10: :: RFUNCT_3:def 10

( dom it = dom F & ( for d being Element of D st d in dom it holds

it . d = max+ (F . d) ) );

existence ( dom it = dom F & ( for d being Element of D st d in dom it holds

it . d = max+ (F . d) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func max- F -> PartFunc of D,REAL means :Def11: :: RFUNCT_3:def 11

( dom it = dom F & ( for d being Element of D st d in dom it holds

it . d = max- (F . d) ) );

existence ( dom it = dom F & ( for d being Element of D st d in dom it holds

it . d = max- (F . d) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for D being non empty set

for F, b_{3} being PartFunc of D,REAL holds

( b_{3} = max+ F iff ( dom b_{3} = dom F & ( for d being Element of D st d in dom b_{3} holds

b_{3} . d = max+ (F . d) ) ) );

for D being non empty set

for F, b

( b

b

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

for D being non empty set

for F, b_{3} being PartFunc of D,REAL holds

( b_{3} = max- F iff ( dom b_{3} = dom F & ( for d being Element of D st d in dom b_{3} holds

b_{3} . d = max- (F . d) ) ) );

for D being non empty set

for F, b

( b

b

theorem :: RFUNCT_3:34

for D being non empty set

for F being PartFunc of D,REAL holds

( F = (max+ F) - (max- F) & abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )

for F being PartFunc of D,REAL holds

( F = (max+ F) - (max- F) & abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )

proof end;

theorem Th35: :: RFUNCT_3:35

for D being non empty set

for F being PartFunc of D,REAL

for r being Real st 0 < r holds

F " {r} = (max+ F) " {r}

for F being PartFunc of D,REAL

for r being Real st 0 < r holds

F " {r} = (max+ F) " {r}

proof end;

theorem Th36: :: RFUNCT_3:36

for D being non empty set

for F being PartFunc of D,REAL holds F " (left_closed_halfline 0) = (max+ F) " {0}

for F being PartFunc of D,REAL holds F " (left_closed_halfline 0) = (max+ F) " {0}

proof end;

theorem Th37: :: RFUNCT_3:37

for D being non empty set

for F being PartFunc of D,REAL

for d being Element of D holds 0 <= (max+ F) . d

for F being PartFunc of D,REAL

for d being Element of D holds 0 <= (max+ F) . d

proof end;

theorem Th38: :: RFUNCT_3:38

for D being non empty set

for F being PartFunc of D,REAL

for r being Real st 0 < r holds

F " {(- r)} = (max- F) " {r}

for F being PartFunc of D,REAL

for r being Real st 0 < r holds

F " {(- r)} = (max- F) " {r}

proof end;

theorem Th39: :: RFUNCT_3:39

for D being non empty set

for F being PartFunc of D,REAL holds F " (right_closed_halfline 0) = (max- F) " {0}

for F being PartFunc of D,REAL holds F " (right_closed_halfline 0) = (max- F) " {0}

proof end;

theorem Th40: :: RFUNCT_3:40

for D being non empty set

for F being PartFunc of D,REAL

for d being Element of D holds 0 <= (max- F) . d

for F being PartFunc of D,REAL

for d being Element of D holds 0 <= (max- F) . d

proof end;

theorem :: RFUNCT_3:41

for D, C being non empty set

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds

max+ F, max+ G are_fiberwise_equipotent

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds

max+ F, max+ G are_fiberwise_equipotent

proof end;

theorem :: RFUNCT_3:42

for D, C being non empty set

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds

max- F, max- G are_fiberwise_equipotent

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds

max- F, max- G are_fiberwise_equipotent

proof end;

registration

let D be non empty set ;

let F be finite PartFunc of D,REAL;

coherence

max+ F is finite

max- F is finite

end;
let F be finite PartFunc of D,REAL;

coherence

max+ F is finite

proof end;

coherence max- F is finite

proof end;

theorem :: RFUNCT_3:43

for D, C being non empty set

for F being finite PartFunc of D,REAL

for G being finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent holds

F,G are_fiberwise_equipotent

for F being finite PartFunc of D,REAL

for G being finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent holds

F,G are_fiberwise_equipotent

proof end;

theorem Th44: :: RFUNCT_3:44

for D being non empty set

for F being PartFunc of D,REAL

for X being set holds (max+ F) | X = max+ (F | X)

for F being PartFunc of D,REAL

for X being set holds (max+ F) | X = max+ (F | X)

proof end;

theorem :: RFUNCT_3:45

for D being non empty set

for F being PartFunc of D,REAL

for X being set holds (max- F) | X = max- (F | X)

for F being PartFunc of D,REAL

for X being set holds (max- F) | X = max- (F | X)

proof end;

theorem Th46: :: RFUNCT_3:46

for D being non empty set

for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds

F . d >= 0 ) holds

max+ F = F

for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds

F . d >= 0 ) holds

max+ F = F

proof end;

theorem :: RFUNCT_3:47

for D being non empty set

for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds

F . d <= 0 ) holds

max- F = - F

for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds

F . d <= 0 ) holds

max- F = - F

proof end;

theorem :: RFUNCT_3:49

for D being non empty set

for F being PartFunc of D,REAL

for r being Real

for X being set holds (F | X) - r = (F - r) | X

for F being PartFunc of D,REAL

for r being Real

for X being set holds (F | X) - r = (F - r) | X

proof end;

theorem Th50: :: RFUNCT_3:50

for D being non empty set

for F being PartFunc of D,REAL

for r, s being Real holds F " {(s + r)} = (F - r) " {s}

for F being PartFunc of D,REAL

for r, s being Real holds F " {(s + r)} = (F - r) " {s}

proof end;

theorem :: RFUNCT_3:51

for D, C being non empty set

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL

for r being Real holds

( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )

for F being PartFunc of D,REAL

for G being PartFunc of C,REAL

for r being Real holds

( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )

proof end;

:: deftheorem Def12 defines is_convex_on RFUNCT_3:def 12 :

for F being PartFunc of REAL,REAL

for X being set holds

( F is_convex_on X iff ( X c= dom F & ( for p being Real st 0 <= p & p <= 1 holds

for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds

F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) );

for F being PartFunc of REAL,REAL

for X being set holds

( F is_convex_on X iff ( X c= dom F & ( for p being Real st 0 <= p & p <= 1 holds

for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds

F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) );

theorem Th52: :: RFUNCT_3:52

for a, b being Real

for F being PartFunc of REAL,REAL holds

( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F & ( for p being Real st 0 <= p & p <= 1 holds

for r, s being Real st r in [.a,b.] & s in [.a,b.] holds

F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) )

for F being PartFunc of REAL,REAL holds

( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F & ( for p being Real st 0 <= p & p <= 1 holds

for r, s being Real st r in [.a,b.] & s in [.a,b.] holds

F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) )

proof end;

theorem :: RFUNCT_3:53

for a, b being Real

for F being PartFunc of REAL,REAL holds

( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds

((F . x1) - (F . x2)) / (x1 - x2) <= ((F . x2) - (F . x3)) / (x2 - x3) ) ) )

for F being PartFunc of REAL,REAL holds

( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds

((F . x1) - (F . x2)) / (x1 - x2) <= ((F . x2) - (F . x3)) / (x2 - x3) ) ) )

proof end;

theorem :: RFUNCT_3:54

for F being PartFunc of REAL,REAL

for X, Y being set st F is_convex_on X & Y c= X holds

F is_convex_on Y

for X, Y being set st F is_convex_on X & Y c= X holds

F is_convex_on Y

proof end;

theorem :: RFUNCT_3:55

for F being PartFunc of REAL,REAL

for X being set

for r being Real holds

( F is_convex_on X iff F - r is_convex_on X )

for X being set

for r being Real holds

( F is_convex_on X iff F - r is_convex_on X )

proof end;

theorem :: RFUNCT_3:56

for F being PartFunc of REAL,REAL

for X being set

for r being Real st 0 < r holds

( F is_convex_on X iff r (#) F is_convex_on X )

for X being set

for r being Real st 0 < r holds

( F is_convex_on X iff r (#) F is_convex_on X )

proof end;

theorem :: RFUNCT_3:58

for F, G being PartFunc of REAL,REAL

for X being set st F is_convex_on X & G is_convex_on X holds

F + G is_convex_on X

for X being set st F is_convex_on X & G is_convex_on X holds

F + G is_convex_on X

proof end;

theorem Th59: :: RFUNCT_3:59

for F being PartFunc of REAL,REAL

for X being set

for r being Real st F is_convex_on X holds

max+ (F - r) is_convex_on X

for X being set

for r being Real st F is_convex_on X holds

max+ (F - r) is_convex_on X

proof end;

theorem :: RFUNCT_3:62

definition

let D be non empty set ;

let F be PartFunc of D,REAL;

let X be set ;

assume A1: dom (F | X) is finite ;

ex b_{1} being non-increasing FinSequence of REAL st F | X,b_{1} are_fiberwise_equipotent

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

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

end;
let F be PartFunc of D,REAL;

let X be set ;

assume A1: dom (F | X) is finite ;

func FinS (F,X) -> non-increasing FinSequence of REAL means :Def13: :: RFUNCT_3:def 13

F | X,it are_fiberwise_equipotent ;

existence F | X,it are_fiberwise_equipotent ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def13 defines FinS RFUNCT_3:def 13 :

for D being non empty set

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite holds

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

( b_{4} = FinS (F,X) iff F | X,b_{4} are_fiberwise_equipotent );

for D being non empty set

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite holds

for b

( b

theorem Th63: :: RFUNCT_3:63

for D being non empty set

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite holds

FinS (F,(dom (F | X))) = FinS (F,X)

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite holds

FinS (F,(dom (F | X))) = FinS (F,X)

proof end;

theorem Th64: :: RFUNCT_3:64

for D being non empty set

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite holds

FinS ((F | X),X) = FinS (F,X)

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite holds

FinS ((F | X),X) = FinS (F,X)

proof end;

theorem Th65: :: RFUNCT_3:65

for D being non empty set

for d being Element of D

for X being set

for F being PartFunc of D,REAL st X is finite & d in dom (F | X) holds

(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent

for d being Element of D

for X being set

for F being PartFunc of D,REAL st X is finite & d in dom (F | X) holds

(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent

proof end;

theorem Th66: :: RFUNCT_3:66

for D being non empty set

for d being Element of D

for X being set

for F being PartFunc of D,REAL st dom (F | X) is finite & d in dom (F | X) holds

(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent

for d being Element of D

for X being set

for F being PartFunc of D,REAL st dom (F | X) is finite & d in dom (F | X) holds

(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent

proof end;

theorem Th67: :: RFUNCT_3:67

for D being non empty set

for F being PartFunc of D,REAL

for X being set

for Y being finite set st Y = dom (F | X) holds

len (FinS (F,X)) = card Y

for F being PartFunc of D,REAL

for X being set

for Y being finite set st Y = dom (F | X) holds

len (FinS (F,X)) = card Y

proof end;

theorem Th69: :: RFUNCT_3:69

for D being non empty set

for F being PartFunc of D,REAL

for d being Element of D st d in dom F holds

FinS (F,{d}) = <*(F . d)*>

for F being PartFunc of D,REAL

for d being Element of D st d in dom F holds

FinS (F,{d}) = <*(F . d)*>

proof end;

theorem Th70: :: RFUNCT_3:70

for D being non empty set

for F being PartFunc of D,REAL

for X being set

for d being Element of D st dom (F | X) is finite & d in dom (F | X) & (FinS (F,X)) . (len (FinS (F,X))) = F . d holds

FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*>

for F being PartFunc of D,REAL

for X being set

for d being Element of D st dom (F | X) is finite & d in dom (F | X) & (FinS (F,X)) . (len (FinS (F,X))) = F . d holds

FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*>

proof end;

defpred S

for F being PartFunc of D,REAL

for X, Y being set

for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & $1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds

F . d1 >= F . d2 ) holds

FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)));

Lm3: S

proof end;

Lm4: for n being Element of NAT st S

S

proof end;

theorem :: RFUNCT_3:71

for D being non empty set

for F being PartFunc of D,REAL

for X, Y being set st dom (F | X) is finite & Y c= X & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds

F . d1 >= F . d2 ) holds

FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))

for F being PartFunc of D,REAL

for X, Y being set st dom (F | X) is finite & Y c= X & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds

F . d1 >= F . d2 ) holds

FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))

proof end;

theorem Th72: :: RFUNCT_3:72

for D being non empty set

for F being PartFunc of D,REAL

for r being Real

for X being set

for d being Element of D st dom (F | X) is finite & d in dom (F | X) holds

( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )

for F being PartFunc of D,REAL

for r being Real

for X being set

for d being Element of D st dom (F | X) is finite & d in dom (F | X) holds

( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )

proof end;

theorem Th73: :: RFUNCT_3:73

for D being non empty set

for F being PartFunc of D,REAL

for r being Real

for X being set

for Z being finite set st Z = dom (F | X) holds

FinS ((F - r),X) = (FinS (F,X)) - ((card Z) |-> r)

for F being PartFunc of D,REAL

for r being Real

for X being set

for Z being finite set st Z = dom (F | X) holds

FinS ((F - r),X) = (FinS (F,X)) - ((card Z) |-> r)

proof end;

theorem :: RFUNCT_3:74

for D being non empty set

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds

F . d >= 0 ) holds

FinS ((max+ F),X) = FinS (F,X)

for F being PartFunc of D,REAL

for X being set st dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds

F . d >= 0 ) holds

FinS ((max+ F),X) = FinS (F,X)

proof end;

theorem :: RFUNCT_3:75

for D being non empty set

for F being PartFunc of D,REAL

for X being set

for r being Real

for Z being finite set st Z = dom (F | X) & rng (F | X) = {r} holds

FinS (F,X) = (card Z) |-> r

for F being PartFunc of D,REAL

for X being set

for r being Real

for Z being finite set st Z = dom (F | X) & rng (F | X) = {r} holds

FinS (F,X) = (card Z) |-> r

proof end;

theorem Th76: :: RFUNCT_3:76

for D being non empty set

for F being PartFunc of D,REAL

for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds

FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent

for F being PartFunc of D,REAL

for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds

FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent

proof end;

definition

let D be non empty set ;

let F be PartFunc of D,REAL;

let X be set ;

correctness

coherence

Sum (FinS (F,X)) is Real;

;

end;
let F be PartFunc of D,REAL;

let X be set ;

correctness

coherence

Sum (FinS (F,X)) is Real;

;

:: deftheorem defines Sum RFUNCT_3:def 14 :

for D being non empty set

for F being PartFunc of D,REAL

for X being set holds Sum (F,X) = Sum (FinS (F,X));

for D being non empty set

for F being PartFunc of D,REAL

for X being set holds Sum (F,X) = Sum (FinS (F,X));

theorem Th77: :: RFUNCT_3:77

for D being non empty set

for F being PartFunc of D,REAL

for X being set

for r being Real st dom (F | X) is finite holds

Sum ((r (#) F),X) = r * (Sum (F,X))

for F being PartFunc of D,REAL

for X being set

for r being Real st dom (F | X) is finite holds

Sum ((r (#) F),X) = r * (Sum (F,X))

proof end;

theorem Th78: :: RFUNCT_3:78

for D being non empty set

for F, G being PartFunc of D,REAL

for X being set

for Y being finite set st Y = dom (F | X) & dom (F | X) = dom (G | X) holds

Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))

for F, G being PartFunc of D,REAL

for X being set

for Y being finite set st Y = dom (F | X) & dom (F | X) = dom (G | X) holds

Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))

proof end;

theorem :: RFUNCT_3:79

for D being non empty set

for F, G being PartFunc of D,REAL

for X being set st dom (F | X) is finite & dom (F | X) = dom (G | X) holds

Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))

for F, G being PartFunc of D,REAL

for X being set st dom (F | X) is finite & dom (F | X) = dom (G | X) holds

Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))

proof end;

theorem :: RFUNCT_3:80

for D being non empty set

for F being PartFunc of D,REAL

for X being set

for r being Real

for Y being finite set st Y = dom (F | X) holds

Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))

for F being PartFunc of D,REAL

for X being set

for r being Real

for Y being finite set st Y = dom (F | X) holds

Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))

proof end;

theorem :: RFUNCT_3:81

theorem :: RFUNCT_3:82

for D being non empty set

for F being PartFunc of D,REAL

for d being Element of D st d in dom F holds

Sum (F,{d}) = F . d

for F being PartFunc of D,REAL

for d being Element of D st d in dom F holds

Sum (F,{d}) = F . d

proof end;

theorem :: RFUNCT_3:83

for D being non empty set

for F being PartFunc of D,REAL

for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds

Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))

for F being PartFunc of D,REAL

for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds

Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))

proof end;

theorem :: RFUNCT_3:84

for D being non empty set

for F being PartFunc of D,REAL

for X, Y being set st dom (F | (X \/ Y)) is finite & dom (F | X) misses dom (F | Y) holds

Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))

for F being PartFunc of D,REAL

for X, Y being set st dom (F | (X \/ Y)) is finite & dom (F | X) misses dom (F | Y) holds

Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))

proof end;

:: Partial Functions from a Domain to the Set of Real Numbers

::