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

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
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
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),

theorem :: FUNCSDOM:16

theorem :: FUNCSDOM:17

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

theorem :: FUNCSDOM:22

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
((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,f])
= (RealFuncExtMult(A)).[a+b,f];

theorem :: FUNCSDOM:26

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
((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
((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 =
((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
(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),
is RealLinearSpace;

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

RLSStruct(#Funcs(A,REAL),
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
(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
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;