The abstract of the Mizar article:

Partial Functions from a Domain to the Set of Real Numbers

by

Jaroslaw Kotowicz

Received May 27, 1990

MML identifier: RFUNCT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTFUN1, ARYTM, ARYTM_1, RELAT_1, ARYTM_3, BOOLE, FUNCT_1,
      FINSEQ_1, SEQ_1, ABSVALUE, FUNCT_3, PARTFUN2, RFUNCT_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, FUNCT_1, FUNCT_3, ABSVALUE, RELSET_1, PARTFUN1, PARTFUN2, SEQ_1;
 constructors REAL_1, FUNCT_3, ABSVALUE, PARTFUN1, PARTFUN2, SEQ_1, MEMBERED,
      XBOOLE_0;
 clusters RELSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve x,X,Y for set;
 reserve C for non empty set;
 reserve c for Element of C;
 reserve f,f1,f2,f3,g,g1 for PartFunc of C,REAL;
 reserve r,r1,r2,p,p1 for real number;

canceled;

theorem :: RFUNCT_1:2
0<=p & 0<=r & p<=p1 & r<=r1 implies p*r<=p1*r1;

::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS
::

definition let C;let f1,f2;
 canceled 3;

func f1/f2 -> PartFunc of C,REAL means
:: RFUNCT_1:def 4
dom it = dom f1 /\ (dom f2 \ f2"{0}) &
for c st c in dom it holds it.c = f1.c * (f2.c)";
end;

definition let C; let f;
 canceled 3;

func f^ -> PartFunc of C,REAL means
:: RFUNCT_1:def 8
dom it = dom f \ f"{0} & for c st c in dom it holds it.c = (f.c)";
end;

canceled 8;

theorem :: RFUNCT_1:11
dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0};

theorem :: RFUNCT_1:12
dom (f1(#)f2) \ (f1(#)f2)"{0} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0});

theorem :: RFUNCT_1:13
c in dom (f^) implies f.c <> 0;

theorem :: RFUNCT_1:14
(f^)"{0} = {};

theorem :: RFUNCT_1:15
(abs(f))"{0} = f"{0} & (-f)"{0} = f"{0};

theorem :: RFUNCT_1:16
dom (f^^) = dom (f|(dom (f^)));

theorem :: RFUNCT_1:17
r<>0 implies (r(#)f)"{0} = f"{0};

::
:: BASIC PROPERTIES OF OPERATIONS
::

canceled;

theorem :: RFUNCT_1:19
  (f1 + f2) + f3 = f1 + (f2 + f3);

canceled;

theorem :: RFUNCT_1:21
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3);

theorem :: RFUNCT_1:22
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3;

theorem :: RFUNCT_1:23
  f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2;

theorem :: RFUNCT_1:24
r(#)(f1(#)f2)=r(#)f1(#)f2;

theorem :: RFUNCT_1:25
r(#)(f1(#)f2)=f1(#)(r(#)f2);

theorem :: RFUNCT_1:26
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3;

theorem :: RFUNCT_1:27
  f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2);

theorem :: RFUNCT_1:28
  r(#)(f1 + f2) = r(#)f1 + r(#)f2;

theorem :: RFUNCT_1:29
(r*p)(#)f = r(#)(p(#)f);

theorem :: RFUNCT_1:30
  r(#)(f1 - f2) = r(#)f1 - r(#)f2;

theorem :: RFUNCT_1:31
  f1-f2 = (-1)(#)(f2-f1);

theorem :: RFUNCT_1:32
  f1 - (f2 + f3) = f1 - f2 - f3;

theorem :: RFUNCT_1:33
1(#)f = f;

theorem :: RFUNCT_1:34
  f1 - (f2 - f3) = f1 - f2 + f3;

theorem :: RFUNCT_1:35
  f1 + (f2 - f3) =f1 + f2 - f3;

theorem :: RFUNCT_1:36
abs(f1(#)f2) = abs(f1)(#)abs(f2);

theorem :: RFUNCT_1:37
  abs(r(#)f) = abs(r)(#)abs(f);

theorem :: RFUNCT_1:38
-f = (-1)(#)f;

theorem :: RFUNCT_1:39
-(-f) = f;

theorem :: RFUNCT_1:40
f1 - f2 = f1 + -f2;

theorem :: RFUNCT_1:41
  f1 - (-f2) = f1 + f2;

theorem :: RFUNCT_1:42
f^^ = f|(dom (f^));

theorem :: RFUNCT_1:43
(f1(#)f2)^ = (f1^)(#)(f2^);

theorem :: RFUNCT_1:44
r<>0 implies (r(#)f)^ = r" (#) (f^);

theorem :: RFUNCT_1:45
(-f)^ = (-1)(#)(f^);

theorem :: RFUNCT_1:46
(abs(f))^ = abs((f^));

theorem :: RFUNCT_1:47
f/g = f(#) (g^);

theorem :: RFUNCT_1:48
r(#)(g/f) = (r(#)g)/f;

theorem :: RFUNCT_1:49
  (f/g)(#)g = (f|dom(g^));

theorem :: RFUNCT_1:50
(f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1);

theorem :: RFUNCT_1:51
(f1/f2)^ = (f2|dom(f2^))/f1;

theorem :: RFUNCT_1:52
g (#) (f1/f2) = (g (#) f1)/f2;

theorem :: RFUNCT_1:53
  g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1;

theorem :: RFUNCT_1:54
  -f/g = (-f)/g & f/(-g) = -f/g;

theorem :: RFUNCT_1:55
  f1/f + f2/f = (f1 + f2)/f & f1/f - f2/f = (f1 - f2)/f;

theorem :: RFUNCT_1:56
f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g);

theorem :: RFUNCT_1:57
  (f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1);

theorem :: RFUNCT_1:58
  f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g);

theorem :: RFUNCT_1:59
  abs(f1/f2) = abs(f1)/abs(f2);

theorem :: RFUNCT_1:60
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X;

theorem :: RFUNCT_1:61
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#)
 f2|X;

theorem :: RFUNCT_1:62
(-f)|X = -(f|X) & (f^)|X = (f|X)^ & (abs(f))|X = abs((f|X));

theorem :: RFUNCT_1:63
  (f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X;

theorem :: RFUNCT_1:64
  (f1/f2)|X = f1|X / f2|X & (f1/f2)|X = f1|X / f2 &(f1/f2)|X = f1 / f2|X;

theorem :: RFUNCT_1:65
  (r(#)f)|X = r(#)(f|X);

::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::

theorem :: RFUNCT_1:66
(f1 is total & f2 is total iff f1+f2 is total) &
(f1 is total & f2 is total iff f1-f2 is total) &
(f1 is total & f2 is total iff f1(#)f2 is total);

theorem :: RFUNCT_1:67
f is total iff r(#)f is total;

theorem :: RFUNCT_1:68
f is total iff -f is total;

theorem :: RFUNCT_1:69
f is total iff abs(f) is total;

theorem :: RFUNCT_1:70
f^ is total iff f"{0} = {} & f is total;

theorem :: RFUNCT_1:71
f1 is total & f2"{0} = {} & f2 is total iff f1/f2 is total;

theorem :: RFUNCT_1:72
  f1 is total & f2 is total implies (f1+f2).c = f1.c + f2.c &
        (f1-f2).c = f1.c - f2.c & (f1(#)f2).c = f1.c * f2.c;

theorem :: RFUNCT_1:73
  f is total implies (r(#)f).c = r * (f.c);

theorem :: RFUNCT_1:74
  f is total implies (-f).c = - f.c & (abs(f)).c = abs( f.c );

theorem :: RFUNCT_1:75
  f^ is total implies (f^).c = (f.c)";

theorem :: RFUNCT_1:76
  f1 is total & f2^ is total implies (f1/f2).c = f1.c *(f2.c)";

::
:: CHARCTERISTIC FUNCTION OF A SUBSET OF A DOMAIN
::

definition let X,C be set;
  redefine func chi(X,C) -> PartFunc of C,REAL;
end;

theorem :: RFUNCT_1:77
f= chi(X,C) iff ( dom f = C &
    for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0));

theorem :: RFUNCT_1:78
  chi(X,C) is total;

theorem :: RFUNCT_1:79
 c in X iff chi(X,C).c = 1;

theorem :: RFUNCT_1:80
 not c in X iff chi(X,C).c = 0;

theorem :: RFUNCT_1:81
  c in C \ X iff chi(X,C).c = 0;

canceled;

theorem :: RFUNCT_1:83
  chi(C,C).c = 1;

theorem :: RFUNCT_1:84
chi(X,C).c <> 1 iff chi(X,C).c = 0;

theorem :: RFUNCT_1:85
  X misses Y implies chi(X,C) + chi(Y,C) = chi(X \/ Y,C);

theorem :: RFUNCT_1:86
  chi(X,C) (#) chi(Y,C) = chi(X /\ Y,C);

::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::

definition let C; let f,Y;
pred f is_bounded_above_on Y means
:: RFUNCT_1:def 9
  ex r st for c st c in Y /\ dom f holds f.c <= r;
pred f is_bounded_below_on Y means
:: RFUNCT_1:def 10
  ex r st for c st c in Y /\ dom f holds r <= f.c;
end;

definition let C; let f,Y;
pred f is_bounded_on Y means
:: RFUNCT_1:def 11
  f is_bounded_above_on Y & f is_bounded_below_on Y;
end;

canceled 3;

theorem :: RFUNCT_1:90
f is_bounded_on Y iff ex r st for c st c in Y /\ dom f holds abs(f.c)<=r;

theorem :: RFUNCT_1:91
  (Y c= X & f is_bounded_above_on X implies f is_bounded_above_on Y) &
(Y c= X & f is_bounded_below_on X implies f is_bounded_below_on Y) &
(Y c= X & f is_bounded_on X implies f is_bounded_on Y);

theorem :: RFUNCT_1:92
  f is_bounded_above_on X & f is_bounded_below_on Y implies f is_bounded_on X
/\
 Y;

theorem :: RFUNCT_1:93
  X misses dom f implies f is_bounded_on X;

theorem :: RFUNCT_1:94
  0 = r implies r(#)f is_bounded_on Y;

theorem :: RFUNCT_1:95
(f is_bounded_above_on Y & 0<=r implies r(#)f is_bounded_above_on Y) &
(f is_bounded_above_on Y & r<=0 implies r(#)f is_bounded_below_on Y);

theorem :: RFUNCT_1:96
(f is_bounded_below_on Y & 0<=r implies r(#)f is_bounded_below_on Y) &
(f is_bounded_below_on Y & r<=0 implies r(#)f is_bounded_above_on Y);

theorem :: RFUNCT_1:97
f is_bounded_on Y implies r(#)f is_bounded_on Y;

theorem :: RFUNCT_1:98
  abs(f) is_bounded_below_on X;

theorem :: RFUNCT_1:99
f is_bounded_on Y implies abs(f) is_bounded_on Y & -f is_bounded_on Y;

theorem :: RFUNCT_1:100
(f1 is_bounded_above_on X & f2 is_bounded_above_on Y implies
                                 f1+f2 is_bounded_above_on (X /\ Y)) &
(f1 is_bounded_below_on X & f2 is_bounded_below_on Y implies
                                 f1+f2 is_bounded_below_on (X /\ Y)) &
(f1 is_bounded_on X & f2 is_bounded_on Y implies
                                 f1+f2 is_bounded_on (X /\ Y));

theorem :: RFUNCT_1:101
f1 is_bounded_on X & f2 is_bounded_on Y implies
 f1(#)f2 is_bounded_on (X /\ Y) & f1-f2 is_bounded_on X /\ Y;

theorem :: RFUNCT_1:102
f is_bounded_above_on X & f is_bounded_above_on Y implies
 f is_bounded_above_on X \/ Y;

theorem :: RFUNCT_1:103
f is_bounded_below_on X & f is_bounded_below_on Y implies
 f is_bounded_below_on X \/ Y;

theorem :: RFUNCT_1:104
  f is_bounded_on X & f is_bounded_on Y implies
 f is_bounded_on X \/ Y;

theorem :: RFUNCT_1:105
  f1 is_constant_on X & f2 is_constant_on Y implies
 (f1 + f2) is_constant_on (X /\ Y) &
 (f1 - f2) is_constant_on (X /\ Y) &
 (f1 (#) f2) is_constant_on (X /\ Y);

theorem :: RFUNCT_1:106
f is_constant_on Y implies p(#)f is_constant_on Y;

theorem :: RFUNCT_1:107
f is_constant_on Y implies abs(f) is_constant_on Y &
                            -f is_constant_on Y;

theorem :: RFUNCT_1:108
f is_constant_on Y implies f is_bounded_on Y;

theorem :: RFUNCT_1:109
  f is_constant_on Y implies (for r holds r(#)f is_bounded_on Y) &
                            (-f is_bounded_on Y) &
                            abs(f) is_bounded_on Y;

theorem :: RFUNCT_1:110
(f1 is_bounded_above_on X & f2 is_constant_on Y implies
       f1+f2 is_bounded_above_on (X /\ Y)) &
(f1 is_bounded_below_on X & f2 is_constant_on Y implies
       f1+f2 is_bounded_below_on (X /\ Y)) &
(f1 is_bounded_on X & f2 is_constant_on Y implies
       f1+f2 is_bounded_on (X /\ Y));

theorem :: RFUNCT_1:111
  (f1 is_bounded_above_on X & f2 is_constant_on Y implies
          f1-f2 is_bounded_above_on (X /\ Y)) &
(f1 is_bounded_below_on X & f2 is_constant_on Y implies
          f1-f2 is_bounded_below_on X /\ Y) &
(f1 is_bounded_on X & f2 is_constant_on Y implies
          f1-f2 is_bounded_on X /\ Y &
          f2-f1 is_bounded_on X /\ Y & f1(#)f2 is_bounded_on X /\ Y);