:: The Relevance of Measure and Probability and Definition of Completenessof Probability
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received November 23, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))
theorem Th1: :: PROB_4:1
theorem Th2: :: PROB_4:2
theorem :: PROB_4:3
canceled;
theorem Th4: :: PROB_4:4
theorem Th5: :: PROB_4:5
theorem Th6: :: PROB_4:6
theorem Th7: :: PROB_4:7
theorem Th8: :: PROB_4:8
theorem Th9: :: PROB_4:9
theorem Th10: :: PROB_4:10
theorem Th11: :: PROB_4:11
theorem Th12: :: PROB_4:12
theorem Th13: :: PROB_4:13
theorem Th14: :: PROB_4:14
:: deftheorem defines P2M PROB_4:def 1 :
theorem Th15: :: PROB_4:15
:: deftheorem defines M2P PROB_4:def 2 :
Lm2:
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Union A1) . n = A1 . n
theorem Th16: :: PROB_4:16
theorem Th17: :: PROB_4:17
theorem :: PROB_4:18
theorem Th19: :: PROB_4:19
theorem :: PROB_4:20
theorem :: PROB_4:21
theorem :: PROB_4:22
:: deftheorem Def3 defines is_complete PROB_4:def 3 :
theorem :: PROB_4:23
:: deftheorem Def4 defines thin PROB_4:def 4 :
theorem Th24: :: PROB_4:24
theorem Th25: :: PROB_4:25
theorem Th26: :: PROB_4:26
:: deftheorem Def5 defines COM PROB_4:def 5 :
theorem Th27: :: PROB_4:27
theorem Th28: :: PROB_4:28
:: deftheorem defines P_COM2M_COM PROB_4:def 6 :
theorem Th29: :: PROB_4:29
:: deftheorem Def7 defines ProbPart PROB_4:def 7 :
theorem :: PROB_4:30
theorem :: PROB_4:31
theorem Th32: :: PROB_4:32
theorem Th33: :: PROB_4:33
theorem Th34: :: PROB_4:34
theorem Th35: :: PROB_4:35
theorem Th36: :: PROB_4:36
theorem :: PROB_4:37
:: deftheorem Def8 defines COM PROB_4:def 8 :
theorem :: PROB_4:38
theorem :: PROB_4:39
theorem Th40: :: PROB_4:40
theorem Th41: :: PROB_4:41
theorem :: PROB_4:42