Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Real Functions Spaces

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

Received March 23, 1990

MML identifier: FUNCSDOM
[ Mizar article, MML identifier index ]

```environ

vocabulary BINOP_1, FUNCT_2, FUNCT_1, QC_LANG1, RELAT_1, FUNCOP_1, VECTSP_1,
RLVECT_1, ARYTM_1, LATTICES, FUNCSDOM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, STRUCT_0, RLVECT_1, REAL_1,
VECTSP_1, FRAENKEL;
constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, VECTSP_1, FRAENKEL,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, RLVECT_1, VECTSP_1, FUNCOP_1, RELSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve x1,x2,z for set;
reserve A,B for non empty set;

definition let A,B; 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;

definition let A,B be non empty set; let f be Function of A,B;
func @f -> Element of Funcs(A,B) equals
:: FUNCSDOM:def 1
f;
end;

reserve f,g,h for Element of Funcs(A,REAL);

definition let X,Z be non empty 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,Z be non empty 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; func RealFuncAdd(A) -> BinOp of Funcs(A,REAL)
means
:: FUNCSDOM:def 2
for f,g being Element of Funcs(A,REAL) holds
it.(f,g) = addreal.:(f,g);
end;

definition let A; func RealFuncMult(A) -> BinOp of Funcs(A,REAL)
means
:: FUNCSDOM:def 3
for f,g being Element of Funcs(A,REAL) holds
it.(f,g) = multreal.:(f,g);
end;

definition let A;
func RealFuncExtMult(A) ->
Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL)
means
:: FUNCSDOM:def 4
for a being Real,
f being (Element of Funcs(A,REAL)), x being (Element of A) holds
(it.[a,f]).x = a*(f.x);
end;

definition let A;
func RealFuncZero(A) -> Element of Funcs(A,REAL) equals
:: FUNCSDOM:def 5
A --> 0;
end;

definition let A;
func RealFuncUnit(A) -> Element of Funcs(A,REAL) equals
:: FUNCSDOM:def 6
A --> 1;
end;

canceled 9;

theorem :: FUNCSDOM:10
h = (RealFuncAdd(A)).(f,g) iff
for x being Element of A holds h.x = f.x + g.x;

theorem :: FUNCSDOM:11
h = (RealFuncMult(A)).(f,g) iff
for x being Element of A holds h.x = f.x * g.x;

theorem :: FUNCSDOM:12
for x being Element of A holds (RealFuncUnit(A)).x = 1;

theorem :: FUNCSDOM:13
for x being Element of A holds (RealFuncZero(A)).x = 0;

theorem :: FUNCSDOM:14
RealFuncZero(A) <> RealFuncUnit(A);

reserve a,b for Real;

theorem :: FUNCSDOM:15
h = (RealFuncExtMult(A)).[a,f] iff
for x being Element of A holds h.x = a*(f.x);

reserve u,v,w for VECTOR of RLSStruct(#Funcs(A,REAL),
(RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#);

theorem :: FUNCSDOM:16
(RealFuncAdd(A)).(f,g) = (RealFuncAdd(A)).(g,f);

theorem :: FUNCSDOM:17
(RealFuncAdd(A)).(f,(RealFuncAdd(A)).(g,h)) =
(RealFuncAdd(A)).((RealFuncAdd(A)).(f,g),h);

theorem :: FUNCSDOM:18
(RealFuncMult(A)).(f,g) = (RealFuncMult(A)).(g,f);

theorem :: FUNCSDOM:19
(RealFuncMult(A)).(f,(RealFuncMult(A)).(g,h)) =
(RealFuncMult(A)).((RealFuncMult(A)).(f,g),h);

theorem :: FUNCSDOM:20
(RealFuncMult(A)).(RealFuncUnit(A),f) = f;

theorem :: FUNCSDOM:21
(RealFuncAdd(A)).(RealFuncZero(A),f) = f;

theorem :: FUNCSDOM:22
(RealFuncAdd(A)).(f,(RealFuncExtMult(A)).[-1,f]) = RealFuncZero(A);

theorem :: FUNCSDOM:23
(RealFuncExtMult(A)).[1,f] = f;

theorem :: FUNCSDOM:24
(RealFuncExtMult(A)).[a,(RealFuncExtMult(A)).[b,f]] =
(RealFuncExtMult(A)).[a*b,f];

theorem :: FUNCSDOM:25
(RealFuncAdd(A)).
((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,f])
= (RealFuncExtMult(A)).[a+b,f];

theorem :: FUNCSDOM:26
(RealFuncMult(A)).(f,(RealFuncAdd(A)).(g,h)) =
(RealFuncAdd(A)).((RealFuncMult(A)).(f,g),(RealFuncMult(A)).(f,h));

theorem :: FUNCSDOM:27
(RealFuncMult(A)).((RealFuncExtMult(A)).[a,f],g) =
(RealFuncExtMult(A)).[a,(RealFuncMult(A)).(f,g)];

theorem :: FUNCSDOM:28
ex f,g st
(for z st z in A holds
(z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
(for z st z in A holds
(z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1));

theorem :: FUNCSDOM:29
(x1 in A & x2 in A & x1<>x2) &
(for z st z in A holds
(z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
(for z st z in A holds
(z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1)) implies
(for a,b st (RealFuncAdd(A)).
((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]) = RealFuncZero(A)
holds a=0 & b=0);

theorem :: FUNCSDOM:30
x1 in A & x2 in A & 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);

theorem :: FUNCSDOM:31
A = {x1,x2} & x1<>x2 &
(for z st z in A holds
(z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
(for z st z in A holds
(z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1))
implies for h holds
(ex a,b st h = (RealFuncAdd(A)).
((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]));

theorem :: FUNCSDOM:32
A = {x1,x2} & x1<>x2 implies ex f,g st
(for h holds
(ex a,b st h =
(RealFuncAdd(A)).
((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g])));

theorem :: FUNCSDOM:33
(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]))));

theorem :: FUNCSDOM:34
RLSStruct(#Funcs(A,REAL),
(RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#)
is RealLinearSpace;

definition let A;
func RealVectSpace(A) -> strict RealLinearSpace equals
:: FUNCSDOM:def 7

RLSStruct(#Funcs(A,REAL),
(RealFuncZero(A)),RealFuncAdd(A),RealFuncExtMult(A)#);
end;

canceled 2;

theorem :: FUNCSDOM:37
ex V being strict RealLinearSpace st
(ex u,v being VECTOR of V st
(for a,b st a*u + b*v = 0.V holds a=0 & b=0) &
(for w being VECTOR of V ex a,b st w = a*u + b*v));

definition
let A;
canceled 4;

func RRing(A) -> strict doubleLoopStr equals
:: FUNCSDOM:def 12
doubleLoopStr(#Funcs(A,REAL),RealFuncAdd(A),RealFuncMult(A),
(RealFuncUnit(A)),(RealFuncZero(A))#);
end;

definition
let A;
cluster RRing A -> non empty;
end;

canceled 4;

theorem :: FUNCSDOM:42
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;

definition
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative right_unital right-distributive
(non empty doubleLoopStr);
end;

definition
mode Ring is Abelian add-associative right_zeroed right_complementable
associative left_unital right_unital
distributive (non empty doubleLoopStr);
end;

theorem :: FUNCSDOM:43
RRing(A) is commutative Ring;

definition
struct(doubleLoopStr,RLSStruct) AlgebraStr (# carrier -> set,
mult,add -> (BinOp of the carrier),
Mult -> (Function of [:REAL,the carrier:],the carrier),
unity,Zero -> Element of the carrier #);
end;

definition
cluster non empty AlgebraStr;
end;

definition let A;
canceled 6;

func RAlgebra(A) -> strict AlgebraStr equals
:: FUNCSDOM:def 19
AlgebraStr(#Funcs(A,REAL),RealFuncMult(A),RealFuncAdd(A),
RealFuncExtMult(A),(RealFuncUnit(A)),(RealFuncZero(A))#);
end;

definition let A;
cluster RAlgebra(A) -> non empty;
end;

canceled 5;

theorem :: FUNCSDOM:49
for x,y,z being Element of RAlgebra(A)
for a,b holds
x+y = y+x &
(x+y)+z = x+(y+z) &
x+(0.RAlgebra(A)) = x &
(ex t being Element of RAlgebra(A) st
x+t=(0.RAlgebra(A))) &
x*y = y*x &
(x*y)*z = x*(y*z) &
x*(1_ RAlgebra(A)) = x &
x*(y+z) = x*y + x*z &
a*(x*y) = (a*x)*y &
a*(x+y) = a*x + a*y &
(a+b)*x = a*x + b*x &
(a*b)*x = a*(b*x);

definition let IT be non empty AlgebraStr;
attr IT is Algebra-like means
:: FUNCSDOM:def 20
for x,y,z being Element of IT
for a,b holds
x*(1_ IT) = x &
x*(y+z) = x*y + x*z &
a*(x*y) = (a*x)*y &
a*(x+y) = a*x + a*y &
(a+b)*x = a*x + b*x &
(a*b)*x = a*(b*x);
end;

definition
cluster strict Abelian add-associative right_zeroed right_complementable
commutative associative Algebra-like (non empty AlgebraStr);
end;

definition
mode Algebra is Abelian add-associative right_zeroed right_complementable
commutative associative Algebra-like (non empty AlgebraStr);
end;

theorem :: FUNCSDOM:50
RAlgebra(A) is Algebra;
```

Back to top