:: Several Properties of the $\sigma$-additive Measure. Discrete categories
:: by J\'ozef Bia{\l}as
::
:: Received July 3, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: MEASURE2:1
:: deftheorem Def1 defines N_Measure_fam MEASURE2:def 1 :
theorem :: MEASURE2:2
canceled;
theorem Th3: :: MEASURE2:3
theorem Th4: :: MEASURE2:4
theorem Th5: :: MEASURE2:5
theorem Th6: :: MEASURE2:6
theorem Th7: :: MEASURE2:7
theorem Th8: :: MEASURE2:8
theorem Th9: :: MEASURE2:9
theorem :: MEASURE2:10
theorem Th11: :: MEASURE2:11
theorem :: MEASURE2:12
canceled;
theorem Th13: :: MEASURE2:13
theorem Th14: :: MEASURE2:14
theorem Th15: :: MEASURE2:15
theorem :: MEASURE2:16
theorem :: MEASURE2:17
theorem :: MEASURE2:18
:: deftheorem Def2 defines non-decreasing MEASURE2:def 2 :
:: deftheorem defines non-increasing MEASURE2:def 3 :
theorem :: MEASURE2:19
canceled;
theorem :: MEASURE2:20
canceled;
theorem :: MEASURE2:21
theorem Th22: :: MEASURE2:22
theorem Th23: :: MEASURE2:23
theorem Th24: :: MEASURE2:24
theorem Th25: :: MEASURE2:25
theorem :: MEASURE2:26
theorem :: MEASURE2:27