:: Real Functions Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received March 23, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem FUNCSDOM:def 1 :
canceled;
definition
let A be
set ;
func RealFuncAdd A -> BinOp of
(Funcs A,REAL ) means :
Def2:
:: FUNCSDOM:def 2
for
f,
g being
Element of
Funcs A,
REAL holds
it . f,
g = addreal .: f,
g;
existence
ex b1 being BinOp of (Funcs A,REAL ) st
for f, g being Element of Funcs A,REAL holds b1 . f,g = addreal .: f,g
uniqueness
for b1, b2 being BinOp of (Funcs A,REAL ) st ( for f, g being Element of Funcs A,REAL holds b1 . f,g = addreal .: f,g ) & ( for f, g being Element of Funcs A,REAL holds b2 . f,g = addreal .: f,g ) holds
b1 = b2
end;
:: deftheorem Def2 defines RealFuncAdd FUNCSDOM:def 2 :
definition
let A be non
empty set ;
func RealFuncMult A -> BinOp of
(Funcs A,REAL ) means :
Def3:
:: FUNCSDOM:def 3
for
f,
g being
Element of
Funcs A,
REAL holds
it . f,
g = multreal .: f,
g;
existence
ex b1 being BinOp of (Funcs A,REAL ) st
for f, g being Element of Funcs A,REAL holds b1 . f,g = multreal .: f,g
uniqueness
for b1, b2 being BinOp of (Funcs A,REAL ) st ( for f, g being Element of Funcs A,REAL holds b1 . f,g = multreal .: f,g ) & ( for f, g being Element of Funcs A,REAL holds b2 . f,g = multreal .: f,g ) holds
b1 = b2
end;
:: deftheorem Def3 defines RealFuncMult FUNCSDOM:def 3 :
definition
let A be
set ;
func RealFuncExtMult A -> Function of
[:REAL ,(Funcs A,REAL ):],
(Funcs A,REAL ) means :
Def4:
:: FUNCSDOM:def 4
for
a being
Real for
f being
Element of
Funcs A,
REAL holds
it . a,
f = multreal [;] a,
f;
existence
ex b1 being Function of [:REAL ,(Funcs A,REAL ):],(Funcs A,REAL ) st
for a being Real
for f being Element of Funcs A,REAL holds b1 . a,f = multreal [;] a,f
uniqueness
for b1, b2 being Function of [:REAL ,(Funcs A,REAL ):],(Funcs A,REAL ) st ( for a being Real
for f being Element of Funcs A,REAL holds b1 . a,f = multreal [;] a,f ) & ( for a being Real
for f being Element of Funcs A,REAL holds b2 . a,f = multreal [;] a,f ) holds
b1 = b2
end;
:: deftheorem Def4 defines RealFuncExtMult FUNCSDOM:def 4 :
:: deftheorem defines RealFuncZero FUNCSDOM:def 5 :
:: deftheorem defines RealFuncUnit FUNCSDOM:def 6 :
Lm1:
for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
theorem :: FUNCSDOM:1
canceled;
theorem :: FUNCSDOM:2
canceled;
theorem :: FUNCSDOM:3
canceled;
theorem :: FUNCSDOM:4
canceled;
theorem :: FUNCSDOM:5
canceled;
theorem :: FUNCSDOM:6
canceled;
theorem :: FUNCSDOM:7
canceled;
theorem :: FUNCSDOM:8
canceled;
theorem :: FUNCSDOM:9
canceled;
theorem Th10: :: FUNCSDOM:10
theorem Th11: :: FUNCSDOM:11
theorem :: FUNCSDOM:12
canceled;
theorem :: FUNCSDOM:13
canceled;
theorem :: FUNCSDOM:14
theorem Th15: :: FUNCSDOM:15
theorem Th16: :: FUNCSDOM:16
theorem Th17: :: FUNCSDOM:17
theorem Th18: :: FUNCSDOM:18
theorem Th19: :: FUNCSDOM:19
theorem Th20: :: FUNCSDOM:20
theorem Th21: :: FUNCSDOM:21
theorem Th22: :: FUNCSDOM:22
theorem Th23: :: FUNCSDOM:23
theorem Th24: :: FUNCSDOM:24
theorem Th25: :: FUNCSDOM:25
Lm2:
for a being Real
for A being set
for f, g being Element of Funcs A,REAL holds (RealFuncAdd A) . ((RealFuncExtMult A) . a,f),((RealFuncExtMult A) . a,g) = (RealFuncExtMult A) . a,((RealFuncAdd A) . f,g)
theorem Th26: :: FUNCSDOM:26
theorem Th27: :: FUNCSDOM:27
theorem Th28: :: FUNCSDOM:28
for
x1 being
set for
A being non
empty set ex
f,
g being
Element of
Funcs A,
REAL st
( ( for
z being
set st
z in A holds
( (
z = x1 implies
f . z = 1 ) & (
z <> x1 implies
f . z = 0 ) ) ) & ( for
z being
set st
z in A holds
( (
z = x1 implies
g . z = 0 ) & (
z <> x1 implies
g . z = 1 ) ) ) )
theorem Th29: :: FUNCSDOM:29
theorem :: FUNCSDOM:30
theorem Th31: :: FUNCSDOM:31
theorem :: FUNCSDOM:32
theorem Th33: :: FUNCSDOM:33
for
x1,
x2 being
set for
A being non
empty set st
A = {x1,x2} &
x1 <> x2 holds
ex
f,
g being
Element of
Funcs A,
REAL st
( ( for
a,
b being
Real st
(RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),
((RealFuncExtMult A) . [b,g]) = RealFuncZero A holds
(
a = 0 &
b = 0 ) ) & ( for
h being
Element of
Funcs A,
REAL ex
a,
b being
Real st
h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),
((RealFuncExtMult A) . [b,g]) ) )
:: deftheorem defines RealVectSpace FUNCSDOM:def 7 :
theorem :: FUNCSDOM:34
canceled;
theorem :: FUNCSDOM:35
canceled;
theorem :: FUNCSDOM:36
canceled;
theorem :: FUNCSDOM:37
definition
let A be non
empty set ;
canceled;canceled;canceled;canceled;func RRing A -> strict doubleLoopStr equals :: FUNCSDOM:def 12
doubleLoopStr(#
(Funcs A,REAL ),
(RealFuncAdd A),
(RealFuncMult A),
(RealFuncUnit A),
(RealFuncZero A) #);
correctness
coherence
doubleLoopStr(# (Funcs A,REAL ),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict doubleLoopStr ;
;
end;
:: deftheorem FUNCSDOM:def 8 :
canceled;
:: deftheorem FUNCSDOM:def 9 :
canceled;
:: deftheorem FUNCSDOM:def 10 :
canceled;
:: deftheorem FUNCSDOM:def 11 :
canceled;
:: deftheorem defines RRing FUNCSDOM:def 12 :
theorem :: FUNCSDOM:38
canceled;
theorem :: FUNCSDOM:39
canceled;
theorem :: FUNCSDOM:40
canceled;
theorem :: FUNCSDOM:41
theorem Th42: :: FUNCSDOM:42
theorem :: FUNCSDOM:43
definition
let A be non
empty set ;
canceled;canceled;canceled;canceled;canceled;canceled;func RAlgebra A -> strict AlgebraStr equals :: FUNCSDOM:def 19
AlgebraStr(#
(Funcs A,REAL ),
(RealFuncMult A),
(RealFuncAdd A),
(RealFuncExtMult A),
(RealFuncUnit A),
(RealFuncZero A) #);
correctness
coherence
AlgebraStr(# (Funcs A,REAL ),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict AlgebraStr ;
;
end;
:: deftheorem FUNCSDOM:def 13 :
canceled;
:: deftheorem FUNCSDOM:def 14 :
canceled;
:: deftheorem FUNCSDOM:def 15 :
canceled;
:: deftheorem FUNCSDOM:def 16 :
canceled;
:: deftheorem FUNCSDOM:def 17 :
canceled;
:: deftheorem FUNCSDOM:def 18 :
canceled;
:: deftheorem defines RAlgebra FUNCSDOM:def 19 :
theorem :: FUNCSDOM:44
theorem :: FUNCSDOM:45
canceled;
theorem :: FUNCSDOM:46
canceled;
theorem :: FUNCSDOM:47
canceled;
theorem :: FUNCSDOM:48
canceled;
theorem Th49: :: FUNCSDOM:49
:: deftheorem Def20 defines Algebra-like FUNCSDOM:def 20 :
Lm5:
for A being non empty set holds RAlgebra A is right_complementable
theorem :: FUNCSDOM:50