:: by Agnes Doll

::

:: Received November 4, 2008

:: Copyright (c) 2008-2019 Association of Mizar Users

theorem Th3: :: KOLMOG01:3

for Omega being non empty set

for X being Subset-Family of Omega st X = {} holds

sigma X = {{},Omega}

for X being Subset-Family of Omega st X = {} holds

sigma X = {{},Omega}

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let B be Subset of Sigma;

let P be Probability of Sigma;

ex b_{1} being Subset of Sigma st

for a being Element of Sigma holds

( a in b_{1} iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )

for b_{1}, b_{2} being Subset of Sigma st ( for a being Element of Sigma holds

( a in b_{1} iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) & ( for a being Element of Sigma holds

( a in b_{2} iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) holds

b_{1} = b_{2}

end;
let Sigma be SigmaField of Omega;

let B be Subset of Sigma;

let P be Probability of Sigma;

func Indep (B,P) -> Subset of Sigma means :Def1: :: KOLMOG01:def 1

for a being Element of Sigma holds

( a in it iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) );

existence for a being Element of Sigma holds

( a in it iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) );

ex b

for a being Element of Sigma holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def1 defines Indep KOLMOG01:def 1 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for B being Subset of Sigma

for P being Probability of Sigma

for b_{5} being Subset of Sigma holds

( b_{5} = Indep (B,P) iff for a being Element of Sigma holds

( a in b_{5} iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for B being Subset of Sigma

for P being Probability of Sigma

for b

( b

( a in b

theorem Th4: :: KOLMOG01:4

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma

for b being Element of B

for f being SetSequence of Sigma st ( for n being Element of NAT

for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V71() holds

P . (b /\ (Union f)) = (P . b) * (P . (Union f))

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma

for b being Element of B

for f being SetSequence of Sigma st ( for n being Element of NAT

for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V71() holds

P . (b /\ (Union f)) = (P . b) * (P . (Union f))

proof end;

theorem Th5: :: KOLMOG01:5

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega

proof end;

theorem Th6: :: KOLMOG01:6

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

proof end;

theorem Th7: :: KOLMOG01:7

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being non empty Subset of Sigma holds

( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P )

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being non empty Subset of Sigma holds

( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P )

proof end;

theorem Th8: :: KOLMOG01:8

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds

B c= Indep (A,P)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds

B c= Indep (A,P)

proof end;

theorem Th9: :: KOLMOG01:9

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds

for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds

for D being Subset-Family of Omega

for sB being non empty Subset of Sigma st D = B & sigma D = sB holds

sigma A c= Indep (sB,P)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds

for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds

for D being Subset-Family of Omega

for sB being non empty Subset of Sigma st D = B & sigma D = sB holds

sigma A c= Indep (sB,P)

proof end;

theorem Th10: :: KOLMOG01:10

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for E, F being Subset-Family of Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds

p,q are_independent_respect_to P ) holds

for u, v being Event of Sigma st u in sigma E & v in sigma F holds

u,v are_independent_respect_to P

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for E, F being Subset-Family of Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds

p,q are_independent_respect_to P ) holds

for u, v being Event of Sigma st u in sigma E & v in sigma F holds

u,v are_independent_respect_to P

proof end;

definition

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

ex b_{1} being Function of I,(bool Sigma) st

for i being set st i in I holds

b_{1} . i is SigmaField of Omega

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

mode ManySortedSigmaField of I,Sigma -> Function of I,(bool Sigma) means :Def2: :: KOLMOG01:def 2

for i being set st i in I holds

it . i is SigmaField of Omega;

existence for i being set st i in I holds

it . i is SigmaField of Omega;

ex b

for i being set st i in I holds

b

proof end;

:: deftheorem Def2 defines ManySortedSigmaField KOLMOG01:def 2 :

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for b_{4} being Function of I,(bool Sigma) holds

( b_{4} is ManySortedSigmaField of I,Sigma iff for i being set st i in I holds

b_{4} . i is SigmaField of Omega );

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for b

( b

b

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let I be set ;

let A be Function of I,Sigma;

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let I be set ;

let A be Function of I,Sigma;

pred A is_independent_wrt P means :: KOLMOG01:def 3

for e being one-to-one FinSequence of I st e <> {} holds

Product ((P * A) * e) = P . (meet (rng (A * e)));

for e being one-to-one FinSequence of I st e <> {} holds

Product ((P * A) * e) = P . (meet (rng (A * e)));

:: deftheorem defines is_independent_wrt KOLMOG01:def 3 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for I being set

for A being Function of I,Sigma holds

( A is_independent_wrt P iff for e being one-to-one FinSequence of I st e <> {} holds

Product ((P * A) * e) = P . (meet (rng (A * e))) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for I being set

for A being Function of I,Sigma holds

( A is_independent_wrt P iff for e being one-to-one FinSequence of I st e <> {} holds

Product ((P * A) * e) = P . (meet (rng (A * e))) );

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let I be set ;

let J be Subset of I;

let F be ManySortedSigmaField of I,Sigma;

ex b_{1} being Function of J,Sigma st

for i being set st i in J holds

b_{1} . i in F . i

end;
let Sigma be SigmaField of Omega;

let I be set ;

let J be Subset of I;

let F be ManySortedSigmaField of I,Sigma;

mode SigmaSection of J,F -> Function of J,Sigma means :Def4: :: KOLMOG01:def 4

for i being set st i in J holds

it . i in F . i;

existence for i being set st i in J holds

it . i in F . i;

ex b

for i being set st i in J holds

b

proof end;

:: deftheorem Def4 defines SigmaSection KOLMOG01:def 4 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for I being set

for J being Subset of I

for F being ManySortedSigmaField of I,Sigma

for b_{6} being Function of J,Sigma holds

( b_{6} is SigmaSection of J,F iff for i being set st i in J holds

b_{6} . i in F . i );

for Omega being non empty set

for Sigma being SigmaField of Omega

for I being set

for J being Subset of I

for F being ManySortedSigmaField of I,Sigma

for b

( b

b

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let I be set ;

let F be ManySortedSigmaField of I,Sigma;

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let I be set ;

let F be ManySortedSigmaField of I,Sigma;

pred F is_independent_wrt P means :: KOLMOG01:def 5

for E being finite Subset of I

for A being SigmaSection of E,F holds A is_independent_wrt P;

for E being finite Subset of I

for A being SigmaSection of E,F holds A is_independent_wrt P;

:: deftheorem defines is_independent_wrt KOLMOG01:def 5 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for I being set

for F being ManySortedSigmaField of I,Sigma holds

( F is_independent_wrt P iff for E being finite Subset of I

for A being SigmaSection of E,F holds A is_independent_wrt P );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for I being set

for F being ManySortedSigmaField of I,Sigma holds

( F is_independent_wrt P iff for E being finite Subset of I

for A being SigmaSection of E,F holds A is_independent_wrt P );

definition

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

let J be Subset of I;

:: original: |

redefine func F | J -> Function of J,(bool Sigma);

coherence

F | J is Function of J,(bool Sigma) by FUNCT_2:32;

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

let J be Subset of I;

:: original: |

redefine func F | J -> Function of J,(bool Sigma);

coherence

F | J is Function of J,(bool Sigma) by FUNCT_2:32;

definition

let I be set ;

let J be Subset of I;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be Function of J,(bool Sigma);

:: original: Union

redefine func Union F -> Subset-Family of Omega;

coherence

Union F is Subset-Family of Omega

end;
let J be Subset of I;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be Function of J,(bool Sigma);

:: original: Union

redefine func Union F -> Subset-Family of Omega;

coherence

Union F is Subset-Family of Omega

proof end;

definition

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

let J be Subset of I;

coherence

sigma (Union (F | J)) is SigmaField of Omega ;

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

let J be Subset of I;

coherence

sigma (Union (F | J)) is SigmaField of Omega ;

:: deftheorem defines sigUn KOLMOG01:def 6 :

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being Subset of I holds sigUn (F,J) = sigma (Union (F | J));

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being Subset of I holds sigUn (F,J) = sigma (Union (F | J));

definition

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

ex b_{1} being Subset-Family of (bool Omega) st

for S being Subset-Family of Omega holds

( S in b_{1} iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) )

for b_{1}, b_{2} being Subset-Family of (bool Omega) st ( for S being Subset-Family of Omega holds

( S in b_{1} iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) & ( for S being Subset-Family of Omega holds

( S in b_{2} iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) holds

b_{1} = b_{2}

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

func futSigmaFields (F,I) -> Subset-Family of (bool Omega) means :Def7: :: KOLMOG01:def 7

for S being Subset-Family of Omega holds

( S in it iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) );

existence for S being Subset-Family of Omega holds

( S in it iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) );

ex b

for S being Subset-Family of Omega holds

( S in b

proof end;

uniqueness for b

( S in b

( S in b

b

proof end;

:: deftheorem Def7 defines futSigmaFields KOLMOG01:def 7 :

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for b_{5} being Subset-Family of (bool Omega) holds

( b_{5} = futSigmaFields (F,I) iff for S being Subset-Family of Omega holds

( S in b_{5} iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) );

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for b

( b

( S in b

registration

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

coherence

not futSigmaFields (F,I) is empty

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

coherence

not futSigmaFields (F,I) is empty

proof end;

definition

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

meet (futSigmaFields (F,I)) is Subset-Family of Omega ;

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

func tailSigmaField (F,I) -> Subset-Family of Omega equals :: KOLMOG01:def 8

meet (futSigmaFields (F,I));

coherence meet (futSigmaFields (F,I));

meet (futSigmaFields (F,I)) is Subset-Family of Omega ;

:: deftheorem defines tailSigmaField KOLMOG01:def 8 :

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) = meet (futSigmaFields (F,I));

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) = meet (futSigmaFields (F,I));

registration

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

coherence

not tailSigmaField (F,I) is empty

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

coherence

not tailSigmaField (F,I) is empty

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let I be non empty set ;

let J be non empty Subset of I;

let F be ManySortedSigmaField of I,Sigma;

ex b_{1} being Subset-Family of Omega st

for x being Subset of Omega holds

( x in b_{1} iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) )

for b_{1}, b_{2} being Subset-Family of Omega st ( for x being Subset of Omega holds

( x in b_{1} iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) ) ) & ( for x being Subset of Omega holds

( x in b_{2} iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) ) ) holds

b_{1} = b_{2}

end;
let Sigma be SigmaField of Omega;

let I be non empty set ;

let J be non empty Subset of I;

let F be ManySortedSigmaField of I,Sigma;

func MeetSections (J,F) -> Subset-Family of Omega means :Def9: :: KOLMOG01:def 9

for x being Subset of Omega holds

( x in it iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) );

existence for x being Subset of Omega holds

( x in it iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) );

ex b

for x being Subset of Omega holds

( x in b

( E c= J & x = meet (rng f) ) )

proof end;

uniqueness for b

( x in b

( E c= J & x = meet (rng f) ) ) ) & ( for x being Subset of Omega holds

( x in b

( E c= J & x = meet (rng f) ) ) ) holds

b

proof end;

:: deftheorem Def9 defines MeetSections KOLMOG01:def 9 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for I being non empty set

for J being non empty Subset of I

for F being ManySortedSigmaField of I,Sigma

for b_{6} being Subset-Family of Omega holds

( b_{6} = MeetSections (J,F) iff for x being Subset of Omega holds

( x in b_{6} iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for I being non empty set

for J being non empty Subset of I

for F being ManySortedSigmaField of I,Sigma

for b

( b

( x in b

( E c= J & x = meet (rng f) ) ) );

theorem Th11: :: KOLMOG01:11

for Omega, I being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)

proof end;

theorem Th12: :: KOLMOG01:12

for Omega, I being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds

P . (a /\ c) = (P . a) * (P . c)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds

P . (a /\ c) = (P . a) * (P . c)

proof end;

theorem Th13: :: KOLMOG01:13

for Omega, I being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma

proof end;

registration

let I, Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

let J be non empty Subset of I;

coherence

MeetSections (J,F) is intersection_stable

end;
let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

let J be non empty Subset of I;

coherence

MeetSections (J,F) is intersection_stable

proof end;

theorem Th14: :: KOLMOG01:14

for Omega, I being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for F being ManySortedSigmaField of I,Sigma

for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds

for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds

P . (u /\ v) = (P . u) * (P . v)

proof end;

definition

let I be set ;

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

ex b_{1} being Subset-Family of Omega st

for S being Subset of Omega holds

( S in b_{1} iff ex E being finite Subset of I st S in sigUn (F,E) )

for b_{1}, b_{2} being Subset-Family of Omega st ( for S being Subset of Omega holds

( S in b_{1} iff ex E being finite Subset of I st S in sigUn (F,E) ) ) & ( for S being Subset of Omega holds

( S in b_{2} iff ex E being finite Subset of I st S in sigUn (F,E) ) ) holds

b_{1} = b_{2}

end;
let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let F be ManySortedSigmaField of I,Sigma;

func finSigmaFields (F,I) -> Subset-Family of Omega means :Def10: :: KOLMOG01:def 10

for S being Subset of Omega holds

( S in it iff ex E being finite Subset of I st S in sigUn (F,E) );

existence for S being Subset of Omega holds

( S in it iff ex E being finite Subset of I st S in sigUn (F,E) );

ex b

for S being Subset of Omega holds

( S in b

proof end;

uniqueness for b

( S in b

( S in b

b

proof end;

:: deftheorem Def10 defines finSigmaFields KOLMOG01:def 10 :

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for b_{5} being Subset-Family of Omega holds

( b_{5} = finSigmaFields (F,I) iff for S being Subset of Omega holds

( S in b_{5} iff ex E being finite Subset of I st S in sigUn (F,E) ) );

for I being set

for Omega being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma

for b

( b

( S in b

theorem Th15: :: KOLMOG01:15

for Omega, I being non empty set

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega

for Sigma being SigmaField of Omega

for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega

proof end;

:: Koenig Lemma

theorem :: KOLMOG01:16

for Omega, I being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

proof end;