:: Dynkin's Lemma in Measure Theory
:: by Franz Merkl
::
:: Received November 27, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: DYNKIN:1
theorem Th2: :: DYNKIN:2
Lm1:
for X being non empty set
for a, b, c being Element of X holds a,b followed_by c is Function of NAT ,X
;
theorem :: DYNKIN:3
canceled;
theorem :: DYNKIN:4
canceled;
theorem :: DYNKIN:5
canceled;
theorem Th6: :: DYNKIN:6
:: deftheorem DYNKIN:def 1 :
canceled;
:: deftheorem Def2 defines seqIntersection DYNKIN:def 2 :
:: deftheorem Def3 defines disjoint_valued DYNKIN:def 3 :
theorem Th7: :: DYNKIN:7
:: deftheorem DYNKIN:def 4 :
canceled;
:: deftheorem defines disjointify DYNKIN:def 5 :
:: deftheorem Def6 defines disjointify DYNKIN:def 6 :
theorem Th8: :: DYNKIN:8
theorem Th9: :: DYNKIN:9
theorem Th10: :: DYNKIN:10
theorem Th11: :: DYNKIN:11
theorem Th12: :: DYNKIN:12
theorem Th13: :: DYNKIN:13
:: deftheorem Def7 defines Dynkin_System DYNKIN:def 7 :
theorem Th14: :: DYNKIN:14
theorem Th15: :: DYNKIN:15
theorem Th16: :: DYNKIN:16
theorem Th17: :: DYNKIN:17
theorem Th18: :: DYNKIN:18
theorem Th19: :: DYNKIN:19
theorem Th20: :: DYNKIN:20
theorem Th21: :: DYNKIN:21
theorem Th22: :: DYNKIN:22
theorem Th23: :: DYNKIN:23
:: deftheorem Def8 defines generated_Dynkin_System DYNKIN:def 8 :
:: deftheorem Def9 defines DynSys DYNKIN:def 9 :
theorem Th24: :: DYNKIN:24
theorem Th25: :: DYNKIN:25
theorem Th26: :: DYNKIN:26
theorem :: DYNKIN:27