:: Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received May 27, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, VALUED_0, FUNCT_1, XCMPLX_0,
ARYTM_1, RELAT_1, ARYTM_3, CARD_1, MEMBERED, PARTFUN1, TARSKI, ORDINAL4,
VALUED_1, COMPLEX1, FUNCT_3, XXREAL_2, XXREAL_0, REAL_1, FUNCT_7,
XREAL_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_3, VALUED_0, VALUED_1, COMSEQ_2, SEQ_2, REAL_1;
constructors PARTFUN1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, VALUED_1,
PARTFUN2, SEQ_2, RELSET_1, COMSEQ_2, XREAL_0;
registrations FUNCT_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0,
VALUED_1, XCMPLX_0, SEQ_2, XXREAL_0, RELAT_1, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
begin
reserve x for object, X,Y for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,f1,f2,f3,g,g1 for complex-valued Function;
reserve r,p for Complex;
::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS
::
definition
let f1,f2 be complex-valued Function;
func f1/f2 -> Function means
:: RFUNCT_1:def 1
dom it = dom f1 /\ (dom f2 \ f2"{0}) &
for c being object st c in dom it holds it.c = f1.c * (f2.c)";
end;
registration
let f1, f2 be complex-valued Function;
cluster f1/f2 -> complex-valued;
end;
registration
let f1, f2 be real-valued Function;
cluster f1/f2 -> real-valued;
end;
definition
let C be set, D be complex-membered set;
let f1, f2 be PartFunc of C,D;
redefine func f1/f2 -> PartFunc of C,COMPLEX;
end;
definition
let C be set, D be real-membered set;
let f1, f2 be PartFunc of C,D;
redefine func f1/f2 -> PartFunc of C,REAL;
end;
definition
let f be complex-valued Function;
func f^ -> Function means
:: RFUNCT_1:def 2
dom it = dom f \ f"{0} &
for c being object st c in dom it holds it.c = (f.c)";
end;
registration
let f be complex-valued Function;
cluster f^ -> complex-valued;
end;
registration
let f be real-valued Function;
cluster f^ -> real-valued;
end;
definition
let C be set, D be complex-membered set, f be PartFunc of C,D;
redefine func f^ -> PartFunc of C,COMPLEX;
end;
definition
let C be set, D be real-membered set, f be PartFunc of C,D;
redefine func f^ -> PartFunc of C,REAL;
end;
theorem :: RFUNCT_1:1
dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0};
theorem :: RFUNCT_1:2
dom (f1(#)f2) \ (f1(#)f2)"{0} = (dom f1 \ f1"{0}) /\ (dom f2 \ f2"{0});
theorem :: RFUNCT_1:3
c in dom (f^) implies f.c <> 0;
theorem :: RFUNCT_1:4
(f^)"{0} = {};
theorem :: RFUNCT_1:5
(abs(f))"{0} = f"{0} & (-f)"{0} = f"{0};
theorem :: RFUNCT_1:6
dom (f^^) = dom (f|(dom (f^)));
theorem :: RFUNCT_1:7
r<>0 implies (r(#)f)"{0} = f"{0};
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem :: RFUNCT_1:8
(f1 + f2) + f3 = f1 + (f2 + f3);
theorem :: RFUNCT_1:9
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3);
theorem :: RFUNCT_1:10
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3;
theorem :: RFUNCT_1:11
f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2;
theorem :: RFUNCT_1:12
r(#)(f1(#)f2)=r(#)f1(#)f2;
theorem :: RFUNCT_1:13
r(#)(f1(#)f2)=f1(#)(r(#)f2);
theorem :: RFUNCT_1:14
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3;
theorem :: RFUNCT_1:15
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2);
theorem :: RFUNCT_1:16
r(#)(f1 + f2) = r(#)f1 + r(#)f2;
theorem :: RFUNCT_1:17
(r*p)(#)f = r(#)(p(#)f);
theorem :: RFUNCT_1:18
r(#)(f1 - f2) = r(#)f1 - r(#)f2;
theorem :: RFUNCT_1:19
f1-f2 = (-1)(#)(f2-f1);
theorem :: RFUNCT_1:20
f1 - (f2 + f3) = f1 - f2 - f3;
theorem :: RFUNCT_1:21
1(#)f = f;
theorem :: RFUNCT_1:22
f1 - (f2 - f3) = f1 - f2 + f3;
theorem :: RFUNCT_1:23
f1 + (f2 - f3) = f1 + f2 - f3;
theorem :: RFUNCT_1:24
abs(f1(#)f2) = abs(f1)(#)abs(f2);
theorem :: RFUNCT_1:25
abs(r(#)f) = |.r.|(#)abs(f);
theorem :: RFUNCT_1:26
f^^ = f|(dom (f^));
theorem :: RFUNCT_1:27
(f1(#)f2)^ = (f1^)(#)(f2^);
theorem :: RFUNCT_1:28
r<>0 implies (r(#)f)^ = r" (#) (f^);
theorem :: RFUNCT_1:29
(-f)^ = (-1)(#)(f^);
theorem :: RFUNCT_1:30
(abs(f))^ = abs(f^);
theorem :: RFUNCT_1:31
f/g = f(#) (g^);
theorem :: RFUNCT_1:32
r(#)(g/f) = (r(#)g)/f;
theorem :: RFUNCT_1:33
(f/g)(#)g = (f|dom(g^));
theorem :: RFUNCT_1:34
(f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1);
theorem :: RFUNCT_1:35
(f1/f2)^ = (f2|dom(f2^))/f1;
theorem :: RFUNCT_1:36
g (#) (f1/f2) = (g (#) f1)/f2;
theorem :: RFUNCT_1:37
g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1;
theorem :: RFUNCT_1:38
-f/g = (-f)/g & f/(-g) = -f/g;
theorem :: RFUNCT_1:39
f1/f + f2/f = (f1 + f2)/f & f1/f - f2/f = (f1 - f2)/f;
theorem :: RFUNCT_1:40
f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g);
theorem :: RFUNCT_1:41
(f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1);
theorem :: RFUNCT_1:42
f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g);
theorem :: RFUNCT_1:43
abs(f1/f2) = abs(f1)/abs(f2);
theorem :: RFUNCT_1:44
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X;
theorem :: RFUNCT_1:45
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)
f2)|X = f1 (#) f2|X;
theorem :: RFUNCT_1:46
(-f)|X = -(f|X) & (f^)|X = (f|X)^ & (abs(f))|X = abs((f|X));
theorem :: RFUNCT_1:47
(f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 & (f1-f2)|X = f1 - f2| X;
theorem :: RFUNCT_1:48
(f1/f2)|X = f1|X / f2|X & (f1/f2)|X = f1|X / f2 &(f1/f2)|X = f1 / f2|X;
theorem :: RFUNCT_1:49
(r(#)f)|X = r(#)(f|X);
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::
reserve r,r1,r2,p for Real;
reserve f,f1,f2 for PartFunc of C,REAL;
theorem :: RFUNCT_1:50
(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:51
f is total iff r(#)f is total;
theorem :: RFUNCT_1:52
f is total iff -f is total;
theorem :: RFUNCT_1:53
f is total iff abs(f) is total;
theorem :: RFUNCT_1:54
f^ is total iff f"{0} = {} & f is total;
theorem :: RFUNCT_1:55
f1 is total & f2"{0} = {} & f2 is total iff f1/f2 is total;
theorem :: RFUNCT_1:56
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:57
f is total implies (r(#)f).c = r * (f.c);
theorem :: RFUNCT_1:58
f is total implies (-f).c = - f.c & (abs(f)).c = |.f.c.|;
theorem :: RFUNCT_1:59
f^ is total implies (f^).c = (f.c)";
theorem :: RFUNCT_1:60
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;
registration
let X,C be set;
cluster chi(X,C) -> total for PartFunc of C,REAL;
end;
theorem :: RFUNCT_1:61
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:62
chi(X,C) is total;
theorem :: RFUNCT_1:63
c in X iff chi(X,C).c = 1;
theorem :: RFUNCT_1:64
not c in X iff chi(X,C).c = 0;
theorem :: RFUNCT_1:65
c in C \ X iff chi(X,C).c = 0;
theorem :: RFUNCT_1:66
chi(C,C).c = 1;
theorem :: RFUNCT_1:67
chi(X,C).c <> 1 iff chi(X,C).c = 0;
theorem :: RFUNCT_1:68
X misses Y implies chi(X,C) + chi(Y,C) = chi(X \/ Y,C);
theorem :: RFUNCT_1:69
chi(X,C) (#) chi(Y,C) = chi(X /\ Y,C);
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::
reserve f for real-valued Function;
theorem :: RFUNCT_1:70
f|Y is bounded_above iff ex r st for c being object st c in Y /\
dom f holds f.c <= r;
theorem :: RFUNCT_1:71
f|Y is bounded_below iff ex r st for c being object st c in Y /\
dom f holds r <= f.c;
theorem :: RFUNCT_1:72
f is bounded iff ex r st for c being object st c in dom f holds |.f.c.|<=r;
theorem :: RFUNCT_1:73
f|Y is bounded iff ex r st for c being object st c in Y /\ dom f holds
|.f.c.|<=r;
theorem :: RFUNCT_1:74
(Y c= X & f|X is bounded_above implies f|Y is bounded_above) & (Y c= X
& f|X is bounded_below implies f|Y is bounded_below) & (Y c= X & f|X is bounded
implies f|Y is bounded);
theorem :: RFUNCT_1:75
f|X is bounded_above & f|Y is bounded_below implies f|(X /\ Y) is bounded;
registration
cluster constant -> bounded for real-valued Function;
end;
theorem :: RFUNCT_1:76
X misses dom f implies f|X is bounded;
theorem :: RFUNCT_1:77
(0(#)f)|Y is bounded;
registration
let f be bounded_above real-valued Function, X be set;
cluster f|X -> bounded_above for real-valued Function;
end;
registration
let f be bounded_below real-valued Function, X be set;
cluster f|X -> bounded_below for real-valued Function;
end;
registration
let f be bounded_above real-valued Function;
let r be non negative Real;
cluster r(#)f -> bounded_above for real-valued Function;
end;
registration
let f be bounded_below real-valued Function;
let r be non negative Real;
cluster r(#)f -> bounded_below for real-valued Function;
end;
registration
let f be bounded_above real-valued Function;
let r be non positive Real;
cluster r(#)f -> bounded_below for real-valued Function;
end;
registration
let f be bounded_below real-valued Function;
let r be non positive Real;
cluster r(#)f -> bounded_above for real-valued Function;
end;
theorem :: RFUNCT_1:78
(f|Y is bounded_above & 0<=r implies (r(#)f)|Y is bounded_above)
& (f|Y is bounded_above & r<=0 implies (r(#)f)|Y is bounded_below);
theorem :: RFUNCT_1:79
(f|Y is bounded_below & 0<=r implies (r(#)f)|Y is bounded_below)
& (f|Y is bounded_below & r<=0 implies (r(#)f)|Y is bounded_above);
theorem :: RFUNCT_1:80
f|Y is bounded implies (r(#)f)|Y is bounded;
registration
let f;
cluster abs f -> bounded_below;
end;
theorem :: RFUNCT_1:81
(abs f)|X is bounded_below;
registration
let f be bounded real-valued Function;
cluster abs f -> bounded for real-valued Function;
end;
registration
let f be bounded_above real-valued Function;
cluster -f -> bounded_below for real-valued Function;
end;
theorem :: RFUNCT_1:82
f|Y is bounded implies (abs f)|Y is bounded & (-f)|Y is bounded;
reserve f1,f2 for real-valued Function;
registration
let f1,f2 be bounded_above real-valued Function;
cluster f1+f2 -> bounded_above for real-valued Function;
end;
registration
let f1,f2 be bounded_below real-valued Function;
cluster f1+f2 -> bounded_below for real-valued Function;
end;
theorem :: RFUNCT_1:83
(f1|X is bounded_above & f2|Y is bounded_above implies (f1+f2)|
(X /\ Y) is bounded_above) & (f1|X is bounded_below & f2|Y is bounded_below
implies (f1+f2)|(X /\ Y) is bounded_below) & (f1|X is bounded & f2|Y is bounded
implies (f1+f2)|(X /\ Y) is bounded);
registration
let f1,f2 be bounded real-valued Function;
cluster f1(#)f2 -> bounded for real-valued Function;
end;
theorem :: RFUNCT_1:84
f1|X is bounded & f2|Y is bounded implies (f1(#)f2)|(X /\ Y) is
bounded & (f1-f2)|(X /\ Y) is bounded;
theorem :: RFUNCT_1:85
f|X is bounded_above & f|Y is bounded_above implies f|(X \/ Y)
is bounded_above;
theorem :: RFUNCT_1:86
f|X is bounded_below & f|Y is bounded_below implies f|(X \/ Y)
is bounded_below;
theorem :: RFUNCT_1:87
f|X is bounded & f|Y is bounded implies f|(X \/ Y) is bounded;
reserve f,f1,f2 for PartFunc of C,REAL;
registration
let C;
let f1,f2 be constant PartFunc of C,REAL;
cluster f1+f2 -> constant;
cluster f1-f2 -> constant;
cluster f1(#)f2 -> constant;
end;
theorem :: RFUNCT_1:88
f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
constant & (f1-f2)|(X /\ Y) is constant & (f1(#)f2)|(X /\ Y) is constant;
registration
let C;
let f be constant PartFunc of C,REAL;
cluster -f -> constant;
cluster abs f -> constant;
let p;
cluster p(#)f -> constant;
end;
theorem :: RFUNCT_1:89
f|Y is constant implies (p(#)f)|Y is constant;
theorem :: RFUNCT_1:90
f|Y is constant implies (-f)|Y is constant;
theorem :: RFUNCT_1:91
f|Y is constant implies (abs f)|Y is constant;
theorem :: RFUNCT_1:92
f|Y is constant implies (for r holds (r(#)f)|Y is bounded) & (-f)|Y is
bounded & (abs f)|Y is bounded;
theorem :: RFUNCT_1:93
(f1|X is bounded_above & f2|Y is constant implies (f1+f2)|(X /\ Y) is
bounded_above) & (f1|X is bounded_below & f2|Y is constant implies (f1+f2)|(X
/\ Y) is bounded_below) & (f1|X is bounded & f2|Y is constant implies (f1+f2)|(
X /\ Y) is bounded);
theorem :: RFUNCT_1:94
(f1|X is bounded_above & f2|Y is constant implies (f1-f2)|(X /\ Y) is
bounded_above) & (f1|X is bounded_below & f2|Y is constant implies (f1-f2)|(X
/\ Y) is bounded_below) & (f1|X is bounded & f2|Y is constant implies (f1-f2)|(
X /\ Y) is bounded & (f2-f1)|(X /\ Y) is bounded& (f1(#)f2)|(X /\ Y) is bounded
);