:: Algebra of Vector Functions :: by Hiroshi Yamazaki and Yasunari Shidama :: :: Received October 27, 1992 :: Copyright (c) 1992-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 XBOOLE_0, SUBSET_1, NORMSP_1, PARTFUN1, REAL_1, ARYTM_3, ARYTM_1, RELAT_1, NUMBERS, FUNCT_1, VALUED_1, SUPINF_2, CARD_1, TARSKI, COMPLEX1, XXREAL_0, XXREAL_2, RLVECT_1, VFUNCT_1, ALGSTR_0, BINOP_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PARTFUN2, VALUED_1, COMSEQ_2, SEQ_2, XXREAL_0, STRUCT_0, ALGSTR_0, RLVECT_1, NORMSP_0, NORMSP_1; constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN2, RFUNCT_1, NORMSP_1, VALUED_1, SEQ_2, RELSET_1, COMSEQ_2; registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0, RFUNCT_1, NORMSP_1, RLVECT_1, NORMSP_0, FUNCT_2, ORDINAL1; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x,X,Y for set; reserve C for non empty set; reserve c for Element of C; reserve V for RealNormSpace; reserve f,f1,f2,f3 for PartFunc of C,V; reserve r,r1,r2,p for Real; :: ::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS :: definition let C; let V be non empty addLoopStr; let f1,f2 be PartFunc of C,V; func f1+f2 -> PartFunc of C,V means :: VFUNCT_1:def 1 dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = (f1/.c) + (f2/.c); func f1-f2 -> PartFunc of C,V means :: VFUNCT_1:def 2 dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = (f1/.c) - (f2/.c); end; registration let C; let V be non empty addLoopStr; let f1,f2 be Function of C,V; cluster f1+f2 -> total; cluster f1-f2 -> total; end; definition let C; let V be non empty RLSStruct; let f1 be PartFunc of C,REAL; let f2 be PartFunc of C,V; func f1(#)f2 -> PartFunc of C,V means :: VFUNCT_1:def 3 dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = f1.c * (f2/.c); end; registration let C; let V be non empty RLSStruct; let f1 be Function of C,REAL; let f2 be Function of C,V; cluster f1(#)f2 -> total; end; definition let C; let V be non empty RLSStruct; let f be PartFunc of C,V; let r be Real; func r(#)f -> PartFunc of C,V means :: VFUNCT_1:def 4 dom it = dom f & for c st c in dom it holds it/.c = r * (f/.c); end; registration let C; let V be non empty RLSStruct; let f be Function of C,V; let r; cluster r(#)f -> total; end; definition let C; let V be non empty addLoopStr; let f be PartFunc of C,V; func -f -> PartFunc of C,V means :: VFUNCT_1:def 5 dom it = dom f & for c st c in dom it holds it/.c = -(f/.c); end; registration let C; let V be non empty addLoopStr; let f be Function of C,V; cluster -f -> total; end; theorem :: VFUNCT_1:1 for f1 be PartFunc of C,REAL holds dom (f1(#)f2) \ (f1(#)f2)"{0.V} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}); theorem :: VFUNCT_1:2 (||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V}; theorem :: VFUNCT_1:3 r<>0 implies (r(#)f)"{0.V} = f"{0.V}; :: :: BASIC PROPERTIES OF OPERATIONS :: theorem :: VFUNCT_1:4 for V being Abelian non empty addLoopStr for f1,f2 being PartFunc of C,V holds f1 + f2 = f2 + f1; definition let C; let V be Abelian non empty addLoopStr; let f1,f2 be PartFunc of C,V; redefine func f1+f2; commutativity; end; theorem :: VFUNCT_1:5 for V being add-associative non empty addLoopStr for f1,f2,f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3); theorem :: VFUNCT_1:6 for V being scalar-associative non empty RLSStruct for f1,f2 being PartFunc of C,REAL, f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3); theorem :: VFUNCT_1:7 for V being scalar-distributive non empty RLSStruct for f1,f2 being PartFunc of C,REAL for f3 being Function of C,V holds (f1 + f2) (#) f3 = f1 (#) f3 + f2 (#) f3; theorem :: VFUNCT_1:8 for V being vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,V for f3 being Function of C,REAL holds f3 (#) (f1 + f2) = f3(#)f1 + f3(#)f2; theorem :: VFUNCT_1:9 for V being scalar-associative non empty RLSStruct for f1 being PartFunc of C,REAL for f2 being PartFunc of C,V holds r(#)(f1(#)f2) = r(#)f1(#)f2; theorem :: VFUNCT_1:10 for V being scalar-associative non empty RLSStruct for f1 being PartFunc of C,REAL for f2 being PartFunc of C,V holds r(#)(f1(#)f2) = f1(#)(r(#)f2); theorem :: VFUNCT_1:11 for V being add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,REAL for f3 being Function of C,V holds (f1 - f2)(#)f3 = f1(#)f3 - f2(#)f3; theorem :: VFUNCT_1:12 for V being add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,V for f3 be PartFunc of C,REAL holds f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2); theorem :: VFUNCT_1:13 for V being vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,V holds r(#)(f1 + f2) = r(#)f1 + r(#)f2; theorem :: VFUNCT_1:14 for V being scalar-associative non empty RLSStruct for f being PartFunc of C,V holds (r*p)(#)f = r(#)(p(#)f); theorem :: VFUNCT_1:15 for V being add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,V holds r(#)(f1 - f2) = r(#)f1 - r(#)f2; theorem :: VFUNCT_1:16 for V being add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,V holds f1-f2 = (-1)(#)(f2-f1); theorem :: VFUNCT_1:17 for V being add-associative right_zeroed right_complementable Abelian non empty addLoopStr for f1,f2,f3 being PartFunc of C,V holds f1 - (f2 + f3) = f1 - f2 - f3; theorem :: VFUNCT_1:18 for V being scalar-unital non empty RLSStruct for f being PartFunc of C,V holds 1(#)f = f; theorem :: VFUNCT_1:19 for V being Abelian add-associative right_zeroed right_complementable non empty addLoopStr for f1,f2,f3 being PartFunc of C,V holds f1 - (f2 - f3) = f1 - f2 + f3; theorem :: VFUNCT_1:20 for V being add-associative non empty addLoopStr for f1,f2,f3 being PartFunc of C,V holds f1 + (f2 - f3) = f1 + f2 - f3; theorem :: VFUNCT_1:21 for V being RealNormSpace-like non empty NORMSTR for f1 being PartFunc of C,REAL for f2 being PartFunc of C,V holds ||.f1(#)f2.|| = abs(f1)(#)||.f2.||; theorem :: VFUNCT_1:22 for V being RealNormSpace-like non empty NORMSTR for f being PartFunc of C,V holds ||.r(#)f.|| = |.r.|(#)||.f.||; theorem :: VFUNCT_1:23 for V being add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct for f being PartFunc of C,V holds -f = (-1)(#)f; theorem :: VFUNCT_1:24 for V being add-associative right_zeroed right_complementable non empty addLoopStr for f being PartFunc of C,V holds -(-f) = f; theorem :: VFUNCT_1:25 for V being non empty addLoopStr for f1,f2 being PartFunc of C,V holds f1 - f2 = f1 + -f2; theorem :: VFUNCT_1:26 for V being add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital scalar-associative vector-distributive non empty RLSStruct for f1,f2 being PartFunc of C,V holds f1 - (-f2) = f1 + f2; theorem :: VFUNCT_1:27 (f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X; theorem :: VFUNCT_1:28 for f1 be PartFunc of C,REAL holds (f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#) f2|X; theorem :: VFUNCT_1:29 (-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).||; theorem :: VFUNCT_1:30 (f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X; theorem :: VFUNCT_1:31 (r(#)f)|X = r(#)(f|X); :: :: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO REAL :: theorem :: VFUNCT_1:32 (f1 is total & f2 is total iff f1+f2 is total) & (f1 is total & f2 is total iff f1-f2 is total); theorem :: VFUNCT_1:33 for f1 be PartFunc of C,REAL holds (f1 is total & f2 is total iff f1(#)f2 is total); theorem :: VFUNCT_1:34 f is total iff r(#)f is total; theorem :: VFUNCT_1:35 f is total iff -f is total; theorem :: VFUNCT_1:36 f is total iff ||.f.|| is total; theorem :: VFUNCT_1:37 f1 is total & f2 is total implies (f1+f2)/.c = (f1/.c) + (f2/.c) & (f1-f2)/.c = (f1/.c) - (f2/.c); theorem :: VFUNCT_1:38 for f1 be PartFunc of C,REAL holds f1 is total & f2 is total implies (f1(#)f2)/.c = f1.c * (f2/.c); theorem :: VFUNCT_1:39 f is total implies (r(#)f)/.c = r * (f/.c); theorem :: VFUNCT_1:40 f is total implies (-f)/.c = - f/.c & (||.f.||).c = ||. f/.c .||; :: :: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN TO A NORMED REAL SPACE :: definition let C; let V be non empty NORMSTR; let f be PartFunc of C,V; let Y; pred f is_bounded_on Y means :: VFUNCT_1:def 6 ex r st for c st c in Y /\ dom f holds ||.f/.c.|| <= r; end; theorem :: VFUNCT_1:41 Y c= X & f is_bounded_on X implies f is_bounded_on Y; theorem :: VFUNCT_1:42 X misses dom f implies f is_bounded_on X; theorem :: VFUNCT_1:43 0(#)f is_bounded_on Y; theorem :: VFUNCT_1:44 f is_bounded_on Y implies r(#)f is_bounded_on Y; theorem :: VFUNCT_1:45 f is_bounded_on Y implies ||.f.|||Y is bounded & -f is_bounded_on Y; theorem :: VFUNCT_1:46 f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y); theorem :: VFUNCT_1:47 for f1 be PartFunc of C,REAL holds f1|X is bounded & f2 is_bounded_on Y implies f1(#)f2 is_bounded_on (X /\ Y); theorem :: VFUNCT_1:48 f1 is_bounded_on X & f2 is_bounded_on Y implies f1-f2 is_bounded_on X /\ Y; theorem :: VFUNCT_1:49 f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y; theorem :: VFUNCT_1:50 f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is constant & (f1-f2)|(X /\ Y) is constant; theorem :: VFUNCT_1:51 for f1 be PartFunc of C,REAL holds f1|X is constant & f2|Y is constant implies (f1(#)f2)|(X /\ Y) is constant; theorem :: VFUNCT_1:52 f|Y is constant implies (p(#)f)|Y is constant; theorem :: VFUNCT_1:53 f|Y is constant implies ||.f.|||Y is constant & (-f)|Y is constant; theorem :: VFUNCT_1:54 f|Y is constant implies f is_bounded_on Y; theorem :: VFUNCT_1:55 f|Y is constant implies (for r holds r(#)f is_bounded_on Y) & -f is_bounded_on Y & ||.f.|||Y is bounded; theorem :: VFUNCT_1:56 f1 is_bounded_on X & f2|Y is constant implies f1+f2 is_bounded_on (X /\ Y); theorem :: VFUNCT_1:57 f1 is_bounded_on X & f2|Y is constant implies f1-f2 is_bounded_on X /\ Y & f2-f1 is_bounded_on X /\ Y;