:: 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 );