:: Measurability of Extended Real Valued Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 6, 2000
:: Copyright (c) 2000 Association of Mizar Users
:: deftheorem Def1 defines real-valued MESFUNC2:def 1 :
theorem :: MESFUNC2:1
theorem Th2: :: MESFUNC2:2
theorem Th3: :: MESFUNC2:3
theorem :: MESFUNC2:4
theorem Th5: :: MESFUNC2:5
theorem Th6: :: MESFUNC2:6
theorem Th7: :: MESFUNC2:7
theorem :: MESFUNC2:8
canceled;
theorem Th9: :: MESFUNC2:9
theorem :: MESFUNC2:10
canceled;
theorem Th11: :: MESFUNC2:11
theorem Th12: :: MESFUNC2:12
theorem :: MESFUNC2:13
definition
let C be non
empty set ;
let f be
PartFunc of
C,
ExtREAL ;
deffunc H1(
Element of
C)
-> Element of
ExtREAL =
max (f . $1),
0. ;
func max+ f -> PartFunc of
C,
ExtREAL means :
Def2:
:: MESFUNC2:def 2
(
dom it = dom f & ( for
x being
Element of
C st
x in dom it holds
it . x = max (f . x),
0. ) );
existence
ex b1 being PartFunc of C, ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max (f . x),0. ) )
uniqueness
for b1, b2 being PartFunc of C, ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max (f . x),0. ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max (f . x),0. ) holds
b1 = b2
deffunc H2(
Element of
C)
-> Element of
ExtREAL =
max (- (f . $1)),
0. ;
func max- f -> PartFunc of
C,
ExtREAL means :
Def3:
:: MESFUNC2:def 3
(
dom it = dom f & ( for
x being
Element of
C st
x in dom it holds
it . x = max (- (f . x)),
0. ) );
existence
ex b1 being PartFunc of C, ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max (- (f . x)),0. ) )
uniqueness
for b1, b2 being PartFunc of C, ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max (- (f . x)),0. ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max (- (f . x)),0. ) holds
b1 = b2
end;
:: deftheorem Def2 defines max+ MESFUNC2:def 2 :
:: deftheorem Def3 defines max- MESFUNC2:def 3 :
theorem Th14: :: MESFUNC2:14
theorem Th15: :: MESFUNC2:15
theorem :: MESFUNC2:16
theorem Th17: :: MESFUNC2:17
theorem :: MESFUNC2:18
theorem Th19: :: MESFUNC2:19
theorem Th20: :: MESFUNC2:20
theorem Th21: :: MESFUNC2:21
theorem Th22: :: MESFUNC2:22
theorem :: MESFUNC2:23
theorem :: MESFUNC2:24
theorem :: MESFUNC2:25
theorem :: MESFUNC2:26
theorem :: MESFUNC2:27
theorem :: MESFUNC2:28
theorem :: MESFUNC2:29
theorem :: MESFUNC2:30
canceled;
theorem :: MESFUNC2:31
theorem :: MESFUNC2:32
theorem Th33: :: MESFUNC2:33
theorem :: MESFUNC2:34
:: deftheorem MESFUNC2:def 4 :
canceled;
:: deftheorem Def5 defines is_simple_func_in MESFUNC2:def 5 :
theorem :: MESFUNC2:35
theorem :: MESFUNC2:36
theorem :: MESFUNC2:37