:: Integral of Real-valued Measurable Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received October 27, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: MESFUNC6:1
theorem Th2: :: MESFUNC6:2
theorem :: MESFUNC6:3
theorem :: MESFUNC6:4
theorem :: MESFUNC6:5
theorem :: MESFUNC6:6
theorem :: MESFUNC6:7
theorem :: MESFUNC6:8
theorem :: MESFUNC6:9
theorem :: MESFUNC6:10
theorem :: MESFUNC6:11
:: deftheorem MESFUNC6:def 1 :
canceled;
:: deftheorem MESFUNC6:def 2 :
canceled;
:: deftheorem MESFUNC6:def 3 :
canceled;
:: deftheorem MESFUNC6:def 4 :
canceled;
:: deftheorem MESFUNC6:def 5 :
canceled;
:: deftheorem Def6 defines is_measurable_on MESFUNC6:def 6 :
theorem Th12: :: MESFUNC6:12
theorem Th13: :: MESFUNC6:13
theorem :: MESFUNC6:14
theorem :: MESFUNC6:15
theorem :: MESFUNC6:16
theorem :: MESFUNC6:17
theorem :: MESFUNC6:18
theorem :: MESFUNC6:19
theorem Th20: :: MESFUNC6:20
theorem Th21: :: MESFUNC6:21
theorem :: MESFUNC6:22
theorem Th23: :: MESFUNC6:23
theorem :: MESFUNC6:24
theorem :: MESFUNC6:25
theorem Th26: :: MESFUNC6:26
theorem :: MESFUNC6:27
theorem Th28: :: MESFUNC6:28
theorem :: MESFUNC6:29
theorem Th30: :: MESFUNC6:30
theorem :: MESFUNC6:31
theorem :: MESFUNC6:32
theorem :: MESFUNC6:33
theorem :: MESFUNC6:34
theorem :: MESFUNC6:35
theorem :: MESFUNC6:36
theorem :: MESFUNC6:37
theorem :: MESFUNC6:38
theorem :: MESFUNC6:39
theorem :: MESFUNC6:40
theorem :: MESFUNC6:41
theorem :: MESFUNC6:42
theorem Th43: :: MESFUNC6:43
theorem Th44: :: MESFUNC6:44
theorem :: MESFUNC6:45
theorem Th46: :: MESFUNC6:46
theorem Th47: :: MESFUNC6:47
theorem :: MESFUNC6:48
:: deftheorem Def7 defines is_simple_func_in MESFUNC6:def 7 :
theorem Th49: :: MESFUNC6:49
theorem :: MESFUNC6:50
theorem Th51: :: MESFUNC6:51
theorem Th52: :: MESFUNC6:52
theorem :: MESFUNC6:53
theorem Th54: :: MESFUNC6:54
theorem :: MESFUNC6:55
theorem Th56: :: MESFUNC6:56
theorem :: MESFUNC6:57
theorem Th58: :: MESFUNC6:58
theorem :: MESFUNC6:59
theorem Th60: :: MESFUNC6:60
theorem :: MESFUNC6:61
theorem Th62: :: MESFUNC6:62
theorem :: MESFUNC6:63
theorem :: MESFUNC6:64
theorem :: MESFUNC6:65
theorem :: MESFUNC6:66
theorem :: MESFUNC6:67
theorem :: MESFUNC6:68
theorem :: MESFUNC6:69
theorem Th70: :: MESFUNC6:70
theorem Th71: :: MESFUNC6:71
Lm1:
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X, REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
theorem :: MESFUNC6:72
theorem :: MESFUNC6:73
theorem :: MESFUNC6:74
theorem :: MESFUNC6:75
theorem :: MESFUNC6:76
theorem :: MESFUNC6:77
theorem :: MESFUNC6:78
theorem :: MESFUNC6:79
theorem Th80: :: MESFUNC6:80
theorem :: MESFUNC6:81
:: deftheorem defines Integral MESFUNC6:def 8 :
theorem Th82: :: MESFUNC6:82
theorem :: MESFUNC6:83
theorem :: MESFUNC6:84
theorem :: MESFUNC6:85
theorem :: MESFUNC6:86
theorem :: MESFUNC6:87
theorem :: MESFUNC6:88
theorem :: MESFUNC6:89
:: deftheorem Def9 defines is_integrable_on MESFUNC6:def 9 :
theorem :: MESFUNC6:90
theorem :: MESFUNC6:91
theorem :: MESFUNC6:92
theorem :: MESFUNC6:93
theorem :: MESFUNC6:94
theorem :: MESFUNC6:95
theorem :: MESFUNC6:96
theorem :: MESFUNC6:97
theorem :: MESFUNC6:98
theorem :: MESFUNC6:99
theorem :: MESFUNC6:100
theorem :: MESFUNC6:101
theorem :: MESFUNC6:102
:: deftheorem defines Integral_on MESFUNC6:def 10 :
theorem :: MESFUNC6:103
theorem :: MESFUNC6:104