The abstract of the Mizar article:

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

by

Jaroslaw Kotowicz, and

Yuji Sakai

Received March 15, 1993

MML identifier: RFUNCT_3

[ Mizar article, MML identifier index ]

environ

 vocabulary SQUARE_1, ARYTM, ARYTM_1, ABSVALUE, FINSEQ_1, RELAT_1, FUNCT_1,
      BOOLE, PARTFUN1, ARYTM_3, SEQ_1, RFINSEQ, CARD_1, FUNCOP_1, BINOP_1,
      SUBSET_1, SETWISEO, RLVECT_1, FUNCT_3, TDGROUP, LIMFUNC1, FINSET_1,
      RCOMP_1, PROB_1, FINSEQ_2, RVSUM_1, VECTSP_1, RFUNCT_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      RELAT_1, FUNCT_1, FINSEQ_1, BINOP_1, CARD_1, REAL_1, NAT_1, ABSVALUE,
      FUNCOP_1, SETWISEO, FINSEQ_2, SQUARE_1, RELSET_1, PARTFUN1, FINSEQOP,
      SEQ_1, RFUNCT_1, FINSEQ_4, SETWOP_2, FINSET_1, RVSUM_1, RCOMP_1,
      PARTFUN2, LIMFUNC1, TOPREAL1, RFINSEQ;
 constructors MONOID_1, PROB_1, REAL_1, NAT_1, SETWISEO, FINSEQOP, RFUNCT_1,
      RCOMP_1, PARTFUN2, LIMFUNC1, TOPREAL1, RFINSEQ, FINSOP_1, FINSEQ_4,
      SEQ_1, SEQ_4, MEMBERED, XBOOLE_0;
 clusters FINSET_1, RFINSEQ, PRELAMB, RELSET_1, FINSEQ_2, XREAL_0, PARTFUN1,
      MONOID_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, FINSEQ_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve n,m for Nat,
        r,s for Real,
        x,y for set;
::
::  Nonnegative and Nonpositive Part of a Real Number
::

definition let n,m be Nat;
redefine func min(n,m)->Nat;
end;

definition let r be real number;
func max+ (r) -> Real equals
:: RFUNCT_3:def 1
 max(r,0);
func max- (r) -> Real equals
:: RFUNCT_3:def 2
 max(-r,0);
end;

theorem :: RFUNCT_3:1
for r be real number holds r = max+(r) - max-(r);

theorem :: RFUNCT_3:2
for r be real number holds abs(r) = max+(r) + max-(r);

theorem :: RFUNCT_3:3
for r be real number holds 2*max+(r) = r + abs(r);

theorem :: RFUNCT_3:4
for r,s be real number st 0<=r holds max+(r*s) = r*(max+ s);

theorem :: RFUNCT_3:5
for r,s be real number holds max+(r+s) <= max+(r) + max+(s);

theorem :: RFUNCT_3:6
  for r be real number holds 0 <= max+(r) & 0 <=max-(r);

theorem :: RFUNCT_3:7
for r1,r2, s1,s2 be real number st r1<=s1 & r2<=s2 holds
 max(r1,r2) <= max(s1,s2);

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

theorem :: RFUNCT_3:8
for D be non empty set, F be PartFunc of D,REAL, r,s be real number st
 r <> 0 holds F"{s/r} = (r(#)F)"{s};

theorem :: RFUNCT_3:9
for D be non empty set, F be PartFunc of D,REAL holds (0(#)F)"{0} = dom F;

theorem :: RFUNCT_3:10
for D be non empty set, F be PartFunc of D,REAL, r be Real st 0<r holds
 abs(F)"{r} = F"{-r,r};

theorem :: RFUNCT_3:11
for D be non empty set, F be PartFunc of D,REAL holds abs(F)"{0} = F"{0};

theorem :: RFUNCT_3:12
for D be non empty set, F be PartFunc of D,REAL, r be Real st r<0 holds
 abs(F)"{r} = {};

theorem :: RFUNCT_3:13
for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL,
 r be Real st r <> 0 holds
      F,G are_fiberwise_equipotent iff r(#)F, r(#)G are_fiberwise_equipotent;

theorem :: RFUNCT_3:14
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL
  holds F,G are_fiberwise_equipotent iff -F, -G are_fiberwise_equipotent;

theorem :: RFUNCT_3:15
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL
 st F,G are_fiberwise_equipotent holds abs(F), abs(G) are_fiberwise_equipotent;

definition let X,Y be set;
mode PartFunc-set of X,Y means
:: RFUNCT_3:def 3
for x being Element of it holds x is PartFunc of X,Y;
end;

definition let X,Y be set;
 cluster non empty PartFunc-set of X,Y;
end;

definition let X,Y be set;
 mode PFUNC_DOMAIN of X,Y is non empty PartFunc-set of X,Y;
end;

definition let X,Y be set;
redefine func PFuncs(X,Y) -> PartFunc-set of X,Y;
 let P be non empty PartFunc-set of X,Y;
  mode Element of P -> PartFunc of X,Y;
end;

definition let D,C be non empty set,
               X be Subset of D,
               c be Element of C;
redefine func X --> c -> Element of PFuncs(D,C);
end;

definition let D be non empty set,
               F1,F2 be Element of PFuncs(D,REAL);
redefine func F1+F2 -> Element of PFuncs(D,REAL);
 func F1-F2 -> Element of PFuncs(D,REAL);
 func F1(#)F2 -> Element of PFuncs(D,REAL);
 func F1/F2 -> Element of PFuncs(D,REAL);
end;

definition let D be non empty set,
               F be Element of PFuncs(D,REAL);
redefine func abs(F) -> Element of PFuncs(D,REAL);
 func - F -> Element of PFuncs(D,REAL);
 func F^ -> Element of PFuncs(D,REAL);
end;

definition let D be non empty set,
               F be Element of PFuncs(D,REAL),
               r be real number;
redefine func r(#)F -> Element of PFuncs(D,REAL);
end;

definition let D be non empty set;
func addpfunc(D) -> BinOp of PFuncs(D,REAL) means
:: RFUNCT_3:def 4
for F1,F2 be Element of PFuncs(D,REAL) holds it.(F1,F2) = F1 + F2;
end;

theorem :: RFUNCT_3:16
for D be non empty set holds addpfunc(D) is commutative;

theorem :: RFUNCT_3:17
for D be non empty set holds addpfunc(D) is associative;

theorem :: RFUNCT_3:18
for D be non empty set holds
  [#](D) --> (0 qua Real) is_a_unity_wrt addpfunc(D);

theorem :: RFUNCT_3:19
for D be non empty set holds
  the_unity_wrt addpfunc(D) = [#](D) --> (0 qua Real);

theorem :: RFUNCT_3:20
for D be non empty set holds addpfunc(D) has_a_unity;

definition let D be non empty set,
               f be FinSequence of PFuncs(D,REAL);
func Sum(f) -> Element of PFuncs(D,REAL) equals
:: RFUNCT_3:def 5
 (addpfunc(D)) $$ f;
end;

theorem :: RFUNCT_3:21
for D be non empty set holds Sum(<*> PFuncs(D,REAL) ) = [#](D)-->(0 qua Real);

theorem :: RFUNCT_3:22
for D be non empty set, G be Element of PFuncs(D,REAL) holds Sum <*G*> = G;

theorem :: RFUNCT_3:23
for D be non empty set, f be FinSequence of PFuncs(D,REAL),
   G be Element of PFuncs(D,REAL) holds Sum(f^<*G*>) = Sum f + G;

theorem :: RFUNCT_3:24
for D be non empty set, f1,f2 be FinSequence of PFuncs(D,REAL) holds
  Sum(f1^f2) = Sum f1 + Sum f2;

theorem :: RFUNCT_3:25
  for D be non empty set, f be FinSequence of PFuncs(D,REAL),
   G be Element of PFuncs(D,REAL) holds Sum(<*G*>^f) = G + Sum f;

theorem :: RFUNCT_3:26
for D be non empty set, G1,G2 be Element of PFuncs(D,REAL) holds
   Sum<*G1,G2*> = G1 + G2;

theorem :: RFUNCT_3:27
  for D be non empty set, G1,G2,G3 be Element of PFuncs(D,REAL) holds
   Sum<*G1,G2,G3*> = G1 + G2 + G3;

theorem :: RFUNCT_3:28
  for D be non empty set, f,g be FinSequence of PFuncs(D,REAL)
  st f,g are_fiberwise_equipotent holds Sum f = Sum g;

definition let D be non empty set,
               f be FinSequence;
func CHI(f,D) -> FinSequence of PFuncs(D,REAL) means
:: RFUNCT_3:def 6
len it = len f & for n st n in dom it holds it.n = chi(f.n,D);
end;

definition let D be non empty set,
               f be FinSequence of PFuncs(D,REAL),
               R be FinSequence of REAL;
func R (#) f -> FinSequence of PFuncs(D,REAL) means
:: RFUNCT_3:def 7
len it = min(len R,len f) &
for n st n in dom it
 for F be PartFunc of D,REAL, r st r = R.n & F = f.n holds it.n = r(#)F;
end;

definition let D be non empty set,
               f be FinSequence of PFuncs(D,REAL),
               d be Element of D;
func f#d -> FinSequence of REAL means
:: RFUNCT_3:def 8
len it = len f & for n be Nat, G be Element of PFuncs(D,REAL) st
                          n in dom it & f.n = G holds it.n = G.d;
end;

definition let D,C be non empty set,
               f be FinSequence of PFuncs(D,C),
               d be Element of D;
pred d is_common_for_dom f means
:: RFUNCT_3:def 9
for G be Element of PFuncs(D,C), n be Nat
  st n in dom f & f.n = G holds d in dom G;
end;

theorem :: RFUNCT_3:29
for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D,
 n be Nat st d is_common_for_dom f & n <> 0 holds d is_common_for_dom f|n;

theorem :: RFUNCT_3:30
  for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D,
  n be Nat st d is_common_for_dom f holds d is_common_for_dom f /^ n;

theorem :: RFUNCT_3:31
for D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL)
  st len f <> 0 holds d is_common_for_dom f iff d in dom Sum(f);

theorem :: RFUNCT_3:32
for D be non empty set, f be FinSequence of PFuncs(D,REAL), d be Element of D,
    n be Nat holds (f|n)#d = (f#d)|n;

theorem :: RFUNCT_3:33
for D be non empty set, f be FinSequence, d be Element of D
  holds d is_common_for_dom CHI(f,D);

theorem :: RFUNCT_3:34
for D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL),
 R be FinSequence of REAL
 st d is_common_for_dom f holds d is_common_for_dom R(#)f;

theorem :: RFUNCT_3:35
  for D be non empty set, f be FinSequence, R be FinSequence of REAL,
  d be Element of D holds d is_common_for_dom R(#)CHI(f,D);

theorem :: RFUNCT_3:36
  for D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL)
  st d is_common_for_dom f holds (Sum(f)).d = Sum (f#d);

definition let D be non empty set,
               F be PartFunc of D,REAL;
func max+(F) -> PartFunc of D,REAL means
:: RFUNCT_3:def 10
dom it = dom F & for d be Element of D st d in dom it holds it.d = max+(F.d);
func max-(F) -> PartFunc of D,REAL means
:: RFUNCT_3:def 11
dom it = dom F & for d be Element of D st d in dom it holds it.d = max-(F.d);
end;

theorem :: RFUNCT_3:37
  for D be non empty set, F be PartFunc of D,REAL holds
  F = max+(F) - max-(F) & abs(F) = max+(F) + max-(F) & 2 (#)
 max+(F) = F + abs(F);

theorem :: RFUNCT_3:38
for D be non empty set, F be PartFunc of D,REAL, r be Real
         st 0<r holds F"{r} = max+(F)"{r};

theorem :: RFUNCT_3:39
for D be non empty set, F be PartFunc of D,REAL
    holds F"(left_closed_halfline(0)) = max+(F)"{0};

theorem :: RFUNCT_3:40
for D be non empty set, F be PartFunc of D,REAL, d be Element of D
        st d in dom F holds 0<=(max+ F).d;

theorem :: RFUNCT_3:41
for D be non empty set, F be PartFunc of D,REAL, r be Real
         st 0<r holds F"{-r} = max-(F)"{r};

theorem :: RFUNCT_3:42
for D be non empty set, F be PartFunc of D,REAL
    holds F"(right_closed_halfline(0)) = max-(F)"{0};

theorem :: RFUNCT_3:43
for D be non empty set, F be PartFunc of D,REAL, d be Element of D
        st d in dom F holds 0<=(max- F).d;

theorem :: RFUNCT_3:44
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL
  st F,G are_fiberwise_equipotent holds
     max+(F), max+(G) are_fiberwise_equipotent;

theorem :: RFUNCT_3:45
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL
  st F,G are_fiberwise_equipotent holds
    max-(F), max-(G) are_fiberwise_equipotent;

definition let A,B be set;
 cluster finite PartFunc of A,B;
end;

definition let D be non empty set,
               F be finite PartFunc of D,REAL;
 cluster max+(F) -> finite;
 cluster max-(F) -> finite;
end;

theorem :: RFUNCT_3:46
  for D,C be non empty set,
    F be finite PartFunc of D,REAL, G be 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;

theorem :: RFUNCT_3:47
for D be non empty set, F be PartFunc of D,REAL, X be set
  holds (max+ F)|X = max+ (F|X);

theorem :: RFUNCT_3:48
  for D be non empty set, F be PartFunc of D,REAL, X be set
  holds (max- F)|X = max- (F|X);

theorem :: RFUNCT_3:49
for D be non empty set, F be PartFunc of D,REAL
 st (for d be Element of D st d in dom F holds F.d>=0) holds max+ F = F;

theorem :: RFUNCT_3:50
  for D be non empty set, F be PartFunc of D,REAL
 st (for d be Element of D st d in dom F holds F.d<=0) holds max- F = -F;

definition let D be non empty set,
               F be PartFunc of D,REAL,
               r be Real;
func F - r -> PartFunc of D,REAL means
:: RFUNCT_3:def 12
dom it = dom F &
for d be Element of D st d in dom it holds it.d = F.d - r;
end;

theorem :: RFUNCT_3:51
for D be non empty set, F be PartFunc of D,REAL holds F - 0 = F;

theorem :: RFUNCT_3:52
  for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set holds
  (F|X) - r = (F-r)| X;

theorem :: RFUNCT_3:53
for D be non empty set, F be PartFunc of D,REAL, r,s be Real holds
  F"{s+r} = (F-r)"{s};

theorem :: RFUNCT_3:54
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL,
    r be Real holds
  F, G are_fiberwise_equipotent iff F-r ,G-r are_fiberwise_equipotent;

definition let F be PartFunc of REAL,REAL,
               X be set;
pred F is_convex_on X means
:: RFUNCT_3:def 13
 X c= dom F &
 for p be Real st 0<=p & p<=1 holds
  for r,s be 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;
end;

theorem :: RFUNCT_3:55
for a,b be Real, F be PartFunc of REAL,REAL holds
  F is_convex_on [.a,b.] iff
 [.a,b.] c= dom F & for p be Real st 0<=p & p<=1 holds
  for r,s be Real st r in [.a,b.] & s in [.a,b.] holds
     F.(p*r + (1-p)*s) <= p*F.r + (1-p)*F.s;

theorem :: RFUNCT_3:56
  for a,b be Real, F be PartFunc of REAL,REAL holds
  F is_convex_on [.a,b.] iff
  [.a,b.] c= dom F &
  for x1,x2,x3 be 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);

theorem :: RFUNCT_3:57
  for F be PartFunc of REAL,REAL, X,Y be set st F is_convex_on X & Y c= X holds
 F is_convex_on Y;

theorem :: RFUNCT_3:58
  for F be PartFunc of REAL,REAL, X be set, r be Real holds
    F is_convex_on X iff F-r is_convex_on X;

theorem :: RFUNCT_3:59
  for F be PartFunc of REAL,REAL, X be set, r be Real st 0<r holds
        F is_convex_on X iff r(#)F is_convex_on X;

theorem :: RFUNCT_3:60
  for F be PartFunc of REAL,REAL, X be set st X c= dom F holds 0(#)
F is_convex_on X;

theorem :: RFUNCT_3:61
  for F,G be PartFunc of REAL,REAL, X be set st
 F is_convex_on X & G is_convex_on X holds F+G is_convex_on X;

theorem :: RFUNCT_3:62
for F be PartFunc of REAL,REAL, X be set, r be Real st
 F is_convex_on X holds max+(F-r) is_convex_on X;

theorem :: RFUNCT_3:63
  for F be PartFunc of REAL,REAL, X be set st F is_convex_on X
  holds max+ F is_convex_on X;

theorem :: RFUNCT_3:64
id [#](REAL) is_convex_on REAL;

theorem :: RFUNCT_3:65
  for r be Real holds max+(id [#](REAL) - r) is_convex_on REAL;

definition let D be non empty set,
               F be PartFunc of D,REAL,
               X be set;
assume  dom(F|X) is finite;
func FinS(F,X) -> non-increasing FinSequence of REAL means
:: RFUNCT_3:def 14
  F|X, it are_fiberwise_equipotent;
end;

theorem :: RFUNCT_3:66
for D be non empty set, F be PartFunc of D,REAL, X be set st
 dom(F|X) is finite holds FinS(F,dom(F|X)) = FinS(F,X);

theorem :: RFUNCT_3:67
for D be non empty set, F be PartFunc of D,REAL, X be set st
 dom(F|X) is finite holds FinS(F|X,X) = FinS(F,X);

definition let D be non empty set;
 let F be PartFunc of D,REAL; let X be finite set;
 redefine func F|X -> finite PartFunc of D,REAL;
end;

theorem :: RFUNCT_3:68
for D be non empty set, d be Element of D, X be set, F be 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;

theorem :: RFUNCT_3:69
for D be non empty set, d be Element of D, X be set, F be 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;

theorem :: RFUNCT_3:70
for D be non empty set, F be PartFunc of D,REAL, X be set,
    Y being finite set st Y = dom(F|X)
   holds len FinS(F,X) = card Y;

theorem :: RFUNCT_3:71
for D be non empty set, F be PartFunc of D,REAL holds FinS(F,{}) = <*>REAL;

theorem :: RFUNCT_3:72
for D be non empty set, F be PartFunc of D,REAL, d be Element of D
  st d in dom F holds FinS(F,{d}) = <* F.d *>;

theorem :: RFUNCT_3:73
for D be non empty set, F be PartFunc of D,REAL, X be set, d be 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*>;

theorem :: RFUNCT_3:74
  for D be non empty set, F be PartFunc of D,REAL, X,Y be set st
  dom(F|X) is finite & Y c= X &
  (for d1,d2 be 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);

theorem :: RFUNCT_3:75
for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set,
 d be 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;

theorem :: RFUNCT_3:76
for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set,
    Z being finite set st Z = dom(F|X)
     holds FinS(F-r, X) = FinS(F,X) - (card Z |->r);

theorem :: RFUNCT_3:77
  for D be non empty set, F be PartFunc of D,REAL, X be set st
 dom(F|X) is finite &
 (for d be Element of D st d in dom(F|X) holds F.d>=0) holds
 FinS(max+ F, X) = FinS(F, X);

theorem :: RFUNCT_3:78
  for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real,
  Z be finite set st Z = dom(F|X)
   & rng(F|X) = {r} holds FinS(F, X) = card(Z) |-> r;

theorem :: RFUNCT_3:79
for D be non empty set, F be PartFunc of D,REAL, X,Y be 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;

definition let D be non empty set,
               F be PartFunc of D,REAL,
               X be set;
func Sum(F,X) -> Real equals
:: RFUNCT_3:def 15
  Sum(FinS(F,X));
end;

theorem :: RFUNCT_3:80
for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real
   st dom(F|X) is finite holds Sum(r(#)F,X) = r * Sum(F,X);

theorem :: RFUNCT_3:81
for D be non empty set, F,G be PartFunc of D,REAL, X be set, 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);

theorem :: RFUNCT_3:82
  for D be non empty set, F,G be PartFunc of D,REAL, X be set st
 dom(F|X) is finite & dom(F|X) = dom(G|X) holds Sum(F-G,X) = Sum(F,X) - Sum
(G,X);

theorem :: RFUNCT_3:83
  for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real,
  Y being finite set st Y = dom(F|X)
   holds Sum(F-r,X) = Sum(F,X) - r*card(Y);

theorem :: RFUNCT_3:84
  for D be non empty set, F be PartFunc of D,REAL holds Sum(F,{}) = 0;

theorem :: RFUNCT_3:85
  for D be non empty set, F be PartFunc of D,REAL, d be Element of D st
 d in dom F
  holds Sum(F,{d}) = F.d;

theorem :: RFUNCT_3:86
  for D be non empty set, F be PartFunc of D,REAL, X,Y be set st
 dom(F|(X \/ Y)) is finite & X misses Y holds Sum(F, X \/ Y) = Sum(F,X) + Sum
(F,Y);

theorem :: RFUNCT_3:87
  for D be non empty set, F be PartFunc of D,REAL, X,Y be 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);