:: Kolmogorov's Zero-one Law
:: by Agnes Doll
::
:: Received November 4, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th12: :: KOLMOG01:1
theorem Th15: :: KOLMOG01:2
for
r being
Real holds
( not
r * r = r or
r = 0 or
r = 1 )
theorem Th1: :: KOLMOG01:3
:: deftheorem Def1 defines Indep KOLMOG01:def 1 :
theorem Th2: :: KOLMOG01:4
theorem Th3: :: KOLMOG01:5
theorem Th4: :: KOLMOG01:6
theorem Th5: :: KOLMOG01:7
theorem Th6: :: KOLMOG01:8
theorem Th7: :: KOLMOG01:9
theorem Th8: :: KOLMOG01:10
:: deftheorem Def2 defines ManySortedSigmaField KOLMOG01:def 2 :
:: deftheorem Def3 defines is_independent_wrt KOLMOG01:def 3 :
:: deftheorem Def4 defines SigmaSection KOLMOG01:def 4 :
:: deftheorem Def5 defines is_independent_wrt KOLMOG01:def 5 :
:: deftheorem defines sigUn KOLMOG01:def 6 :
:: deftheorem Def7 defines futSigmaFields KOLMOG01:def 7 :
:: deftheorem defines tailSigmaField KOLMOG01:def 8 :
:: deftheorem Def9 defines MeetSections KOLMOG01:def 9 :
theorem Th9: :: KOLMOG01:11
theorem Th10: :: KOLMOG01:12
theorem Th11: :: KOLMOG01:13
theorem Th14: :: KOLMOG01:14
:: deftheorem Def10 defines finSigmaFields KOLMOG01:def 10 :
theorem Th16: :: KOLMOG01:15
theorem :: KOLMOG01:16