:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received October 15, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: MEASURE1:1
theorem :: MEASURE1:2
canceled;
theorem :: MEASURE1:3
canceled;
theorem Th4: :: MEASURE1:4
theorem Th5: :: MEASURE1:5
theorem :: MEASURE1:6
canceled;
theorem :: MEASURE1:7
theorem :: MEASURE1:8
theorem :: MEASURE1:9
canceled;
theorem :: MEASURE1:10
canceled;
theorem :: MEASURE1:11
canceled;
theorem :: MEASURE1:12
canceled;
theorem :: MEASURE1:13
canceled;
theorem :: MEASURE1:14
canceled;
theorem Th15: :: MEASURE1:15
:: deftheorem MEASURE1:def 1 :
canceled;
:: deftheorem MEASURE1:def 2 :
canceled;
:: deftheorem Def3 defines compl-closed MEASURE1:def 3 :
theorem Th16: :: MEASURE1:16
theorem :: MEASURE1:17
theorem :: MEASURE1:18
theorem Th19: :: MEASURE1:19
theorem Th20: :: MEASURE1:20
theorem :: MEASURE1:21
:: deftheorem Def4 defines nonnegative MEASURE1:def 4 :
theorem :: MEASURE1:22
canceled;
theorem :: MEASURE1:23
canceled;
:: deftheorem Def5 defines additive MEASURE1:def 5 :
theorem :: MEASURE1:24
canceled;
theorem Th25: :: MEASURE1:25
theorem Th26: :: MEASURE1:26
theorem Th27: :: MEASURE1:27
theorem :: MEASURE1:28
canceled;
theorem :: MEASURE1:29
:: deftheorem MEASURE1:def 6 :
canceled;
:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :
theorem :: MEASURE1:30
canceled;
theorem :: MEASURE1:31
theorem :: MEASURE1:32
theorem :: MEASURE1:33
theorem Th34: :: MEASURE1:34
theorem Th35: :: MEASURE1:35
theorem :: MEASURE1:36
canceled;
theorem :: MEASURE1:37
canceled;
theorem Th38: :: MEASURE1:38
theorem :: MEASURE1:39
theorem Th40: :: MEASURE1:40
theorem :: MEASURE1:41
theorem Th42: :: MEASURE1:42
:: deftheorem MEASURE1:def 8 :
canceled;
:: deftheorem Def9 defines sigma-additive MEASURE1:def 9 :
theorem :: MEASURE1:43
canceled;
theorem :: MEASURE1:44
canceled;
theorem :: MEASURE1:45
canceled;
theorem :: MEASURE1:46
canceled;
theorem :: MEASURE1:47
canceled;
theorem :: MEASURE1:48
canceled;
theorem Th49: :: MEASURE1:49
theorem :: MEASURE1:50
canceled;
theorem :: MEASURE1:51
canceled;
theorem Th52: :: MEASURE1:52
theorem Th53: :: MEASURE1:53
theorem Th54: :: MEASURE1:54
theorem Th55: :: MEASURE1:55
theorem :: MEASURE1:56
theorem Th57: :: MEASURE1:57
:: deftheorem MEASURE1:def 10 :
canceled;
:: deftheorem Def11 defines sigma-additive MEASURE1:def 11 :
theorem :: MEASURE1:58
canceled;
theorem :: MEASURE1:59
canceled;
theorem Th60: :: MEASURE1:60
theorem :: MEASURE1:61
theorem Th62: :: MEASURE1:62
theorem :: MEASURE1:63
theorem Th64: :: MEASURE1:64
theorem :: MEASURE1:65
canceled;
theorem :: MEASURE1:66
theorem :: MEASURE1:67
:: deftheorem MEASURE1:def 12 :
canceled;
:: deftheorem Def13 defines measure_zero MEASURE1:def 13 :
theorem :: MEASURE1:68
canceled;
theorem :: MEASURE1:69
theorem :: MEASURE1:70
theorem :: MEASURE1:71