:: Real Functions Spaces :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received March 23, 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 XBOOLE_0, BINOP_1, FUNCT_2, SUBSET_1, FUNCT_1, ZFMISC_1, NUMBERS, RELAT_1, FUNCOP_1, BINOP_2, REAL_1, CARD_1, ARYTM_3, RLVECT_1, ARYTM_1, STRUCT_0, ALGSTR_0, SUPINF_2, GROUP_1, MESFUNC1, VECTSP_1, LATTICES, TARSKI, FUNCSDOM, VALUED_1, VALUED_2, VALUED_0, FUNCT_7, FUNCT_4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, MEMBERED, FUNCT_1, FUNCT_2, BINOP_1, FUNCT_4, DOMAIN_1, FUNCOP_1, BINOP_2, XCMPLX_0, XREAL_0, VALUED_0, VALUED_1, VALUED_2, STRUCT_0, ALGSTR_0, RLVECT_1, REAL_1, GROUP_1, VECTSP_1, PARTFUN3; constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, BINOP_2, VECTSP_1, RLVECT_1, FUNCT_3, RELSET_1, VALUED_2, VALUED_0, VALUED_1, NUMBERS, GROUP_1, PARTFUN3, FUNCT_4; registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, RLVECT_1, VECTSP_1, ALGSTR_0, BINOP_2, FUNCOP_1, FUNCT_3, XREAL_0, RELAT_1, VALUED_0, STRUCT_0, MEMBERED; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x1,x2,z for set; reserve A,B for non empty set; definition let A be set, B be non empty set; let F be BinOp of Funcs(A,B); let f,g be Element of Funcs(A,B); redefine func F.(f,g) -> Element of Funcs(A,B); end; definition let A,B,C,D be non empty set; let F be Function of [:C,D:],Funcs(A,B); let cd be Element of [:C,D:]; redefine func F.cd -> Element of Funcs(A,B); end; reserve f,g,h for Element of Funcs(A,REAL); definition let X be non empty set, Z be set; let F be (BinOp of X), f,g be Function of Z,X; redefine func F.:(f,g) -> Element of Funcs(Z,X); end; definition let X be non empty set, Z be set; let F be (BinOp of X),a be Element of X,f be Function of Z,X; redefine func F[;](a,f) -> Element of Funcs(Z,X); end; definition let A be set; func RealFuncAdd(A) -> BinOp of Funcs(A,REAL) means :: FUNCSDOM:def 1 for f,g being Element of Funcs(A,REAL) holds it.(f,g) = addreal.:(f,g); end; registration let A be set; cluster RealFuncAdd A -> real-functions-valued; end; definition let A be set; func RealFuncMult(A) -> BinOp of Funcs(A,REAL) means :: FUNCSDOM:def 2 for f,g being Element of Funcs(A,REAL) holds it.(f,g) = multreal.:(f,g); end; registration let A be set; cluster RealFuncMult A -> real-functions-valued; end; definition let A be set; func RealFuncExtMult(A) -> Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL) means :: FUNCSDOM:def 3 for a being Real, f being Element of Funcs(A,REAL) holds it.(a,f) = multreal[;](a,f); end; registration let A be set; cluster RealFuncExtMult A -> real-functions-valued; end; definition let A be set; func RealFuncZero A -> Element of Funcs(A,REAL) equals :: FUNCSDOM:def 4 A --> 0; func RealFuncUnit A -> Element of Funcs(A,REAL) equals :: FUNCSDOM:def 5 A --> 1; end; theorem :: FUNCSDOM:1 h = (RealFuncAdd A).(f,g) iff for x being Element of A holds h.x = f.x + g.x; theorem :: FUNCSDOM:2 h = (RealFuncMult(A)).(f,g) iff for x being Element of A holds h.x = f.x * g.x; theorem :: FUNCSDOM:3 RealFuncZero(A) <> RealFuncUnit(A); reserve a,b for Real; theorem :: FUNCSDOM:4 h = (RealFuncExtMult A).[a,f] iff for x being Element of A holds h.x = a*(f.x); theorem :: FUNCSDOM:5 for A being set, f,g being Element of Funcs(A,REAL) holds (RealFuncAdd A).(f,g) = (RealFuncAdd A).(g,f); theorem :: FUNCSDOM:6 for A being set, f,g,h being Element of Funcs(A,REAL) holds (RealFuncAdd A).(f,(RealFuncAdd A).(g,h)) = (RealFuncAdd A).((RealFuncAdd A).(f,g),h); theorem :: FUNCSDOM:7 for A be set, f,g be Element of Funcs(A,REAL) holds (RealFuncMult A).(f,g) = (RealFuncMult A).(g,f); theorem :: FUNCSDOM:8 for A be set, f,g,h be Element of Funcs(A,REAL) holds (RealFuncMult(A)).(f,(RealFuncMult(A)).(g,h)) = (RealFuncMult(A)).((RealFuncMult(A)).(f,g),h); theorem :: FUNCSDOM:9 for A being set, f being Element of Funcs(A,REAL) holds (RealFuncMult(A)).(RealFuncUnit(A),f) = f; theorem :: FUNCSDOM:10 for A being set, f being Element of Funcs(A,REAL) holds (RealFuncAdd A).(RealFuncZero(A),f) = f; theorem :: FUNCSDOM:11 for A being set, f be Element of Funcs(A,REAL) holds (RealFuncAdd A).(f,(RealFuncExtMult A).[-1,f]) = RealFuncZero(A); theorem :: FUNCSDOM:12 for A being set, f being Element of Funcs(A,REAL) holds (RealFuncExtMult A).(1,f) = f; theorem :: FUNCSDOM:13 for A being set, f being Element of Funcs(A,REAL) holds (RealFuncExtMult A).(a,(RealFuncExtMult A).(b,f)) = (RealFuncExtMult A).(a*b,f); theorem :: FUNCSDOM:14 for A being set, f being Element of Funcs(A,REAL) holds (RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(b,f)) = (RealFuncExtMult A).(a+b,f); theorem :: FUNCSDOM:15 for A be set, f,g,h be Element of Funcs(A,REAL) holds (RealFuncMult(A)).(f,(RealFuncAdd A).(g,h)) = (RealFuncAdd A).((RealFuncMult(A)).(f,g),(RealFuncMult(A)).(f,h)); theorem :: FUNCSDOM:16 for A being set, f,g,h be Element of Funcs(A,REAL), a being Real holds (RealFuncMult A).((RealFuncExtMult A).(a,f),g) = (RealFuncExtMult A).(a,(RealFuncMult A).(f,g)); theorem :: FUNCSDOM:17 x1 in A implies (RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) & (RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL); theorem :: FUNCSDOM:18 x1 in A & x2 in A & x1<>x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) implies for a,b st (RealFuncAdd A).((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]) = RealFuncZero(A) holds a=0 & b=0; ::$CT theorem :: FUNCSDOM:20 A = {x1,x2} & x1<>x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) implies for h holds ex a,b st h = (RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]); ::$CT theorem :: FUNCSDOM:22 A = {x1,x2} & x1<>x2 implies ex f,g st (for a,b st (RealFuncAdd A).((RealFuncExtMult A).[a,f], (RealFuncExtMult A).[b,g]) = RealFuncZero(A) holds a=0 & b=0) & for h holds ex a,b st h = (RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]); definition let A be set; func RealVectSpace(A) -> strict RealLinearSpace equals :: FUNCSDOM:def 6 RLSStruct(#Funcs(A,REAL), RealFuncZero(A),RealFuncAdd(A),RealFuncExtMult(A)#); end; theorem :: FUNCSDOM:23 ex V being strict RealLinearSpace st ex u,v being Element of V st (for a,b st a*u + b*v = 0.V holds a=0 & b=0) & for w being Element of V ex a,b st w = a*u + b*v; definition let A; func RRing(A) -> strict doubleLoopStr equals :: FUNCSDOM:def 7 doubleLoopStr(#Funcs(A,REAL), RealFuncAdd A,RealFuncMult A, RealFuncUnit A,RealFuncZero A#); end; registration let A; cluster RRing A -> non empty; end; registration let A; cluster RRing(A) -> unital; end; theorem :: FUNCSDOM:24 1.RRing(A) = RealFuncUnit(A); theorem :: FUNCSDOM:25 for x,y,z being Element of RRing(A) holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.RRing(A)) = x & (ex t being Element of RRing(A) st x+t=(0.RRing( A))) & x*y = y*x & (x*y)*z = x*(y*z) & x*(1.RRing(A)) = x & (1.RRing(A))*x = x & x*(y+z) = x*y + x*z & (y+z)*x = y*x + z*x; registration cluster strict Abelian add-associative right_zeroed right_complementable associative commutative right_unital right-distributive for 1-element doubleLoopStr; end; theorem :: FUNCSDOM:26 RRing(A) is commutative Ring; definition struct (doubleLoopStr,RLSStruct) AlgebraStr (# carrier -> set, multF,addF -> (BinOp of the carrier), Mult -> (Function of [:REAL,the carrier:],the carrier), OneF,ZeroF -> Element of the carrier #); end; registration cluster non empty for AlgebraStr; end; definition let A be set; func RAlgebra A -> strict AlgebraStr equals :: FUNCSDOM:def 8 AlgebraStr(#Funcs(A,REAL), RealFuncMult(A),RealFuncAdd(A), RealFuncExtMult(A),(RealFuncUnit(A)),( RealFuncZero(A))#); end; registration let A; cluster RAlgebra(A) -> non empty; end; registration let A; cluster RAlgebra(A) -> unital; end; theorem :: FUNCSDOM:27 1.RAlgebra(A) = RealFuncUnit(A); definition let IT be non empty AlgebraStr; attr IT is vector-associative means :: FUNCSDOM:def 9 for x,y being Element of IT for a holds a*(x*y) = (a*x)*y; end; registration let A be set; cluster RAlgebra A -> non empty; end; registration let A be set; cluster RAlgebra A -> strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-associative scalar-associative vector-distributive scalar-distributive; end; registration cluster strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-associative scalar-associative vector-distributive scalar-distributive for non empty AlgebraStr; end; definition mode Algebra is Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-associative scalar-associative vector-distributive scalar-distributive non empty AlgebraStr; end; theorem :: FUNCSDOM:28 (RealFuncAdd A).(f,g) = f + g; theorem :: FUNCSDOM:29 (RealFuncMult(A)).(f,g) = f (#) g; theorem :: FUNCSDOM:30 (RealFuncExtMult A).(a,f) = a (#) f;