let Omega be non empty set ; :: thesis: 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

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

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

let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega

let B be non empty Subset of Sigma; :: thesis: Indep (B,P) is Dynkin_System of Omega

A1: for b being Element of B holds P . ({} /\ b) = (P . {}) * (P . b)

{} is Element of Sigma by PROB_1:22;

then A2: {} in Indep (B,P) by A1, Def1;

A3: for g being SetSequence of Omega st rng g c= Indep (B,P) & g is V71() holds

Union g in Indep (B,P)

Z ` in Indep (B,P)

hence Indep (B,P) is Dynkin_System of Omega ; :: thesis: verum

for P being Probability of Sigma

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

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

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

let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega

let B be non empty Subset of Sigma; :: thesis: Indep (B,P) is Dynkin_System of Omega

A1: for b being Element of B holds P . ({} /\ b) = (P . {}) * (P . b)

proof

reconsider Indp = Indep (B,P) as Subset-Family of Omega by XBOOLE_1:1;
let b be Element of B; :: thesis: P . ({} /\ b) = (P . {}) * (P . b)

reconsider b = b as Event of Sigma ;

P . ({} /\ b) = 0 by VALUED_0:def 19;

hence P . ({} /\ b) = (P . {}) * (P . b) ; :: thesis: verum

end;reconsider b = b as Event of Sigma ;

P . ({} /\ b) = 0 by VALUED_0:def 19;

hence P . ({} /\ b) = (P . {}) * (P . b) ; :: thesis: verum

{} is Element of Sigma by PROB_1:22;

then A2: {} in Indep (B,P) by A1, Def1;

A3: for g being SetSequence of Omega st rng g c= Indep (B,P) & g is V71() holds

Union g in Indep (B,P)

proof

for Z being Subset of Omega st Z in Indep (B,P) holds
let g be SetSequence of Omega; :: thesis: ( rng g c= Indep (B,P) & g is V71() implies Union g in Indep (B,P) )

assume that

A4: rng g c= Indep (B,P) and

A5: g is V71() ; :: thesis: Union g in Indep (B,P)

reconsider Ug = Union g as Element of Sigma by PROB_1:26;

for n being Element of NAT

for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)

hence Union g in Indep (B,P) by Def1; :: thesis: verum

end;assume that

A4: rng g c= Indep (B,P) and

A5: g is V71() ; :: thesis: Union g in Indep (B,P)

now :: thesis: for n being Nat holds g . n is Event of Sigma

then reconsider g = g as SetSequence of Sigma by PROB_1:25;let n be Nat; :: thesis: g . n is Event of Sigma

g . n is Element of Sigma

end;g . n is Element of Sigma

proof
end;

hence
g . n is Event of Sigma
; :: thesis: verumreconsider Ug = Union g as Element of Sigma by PROB_1:26;

for n being Element of NAT

for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)

proof

then
for b being Element of B holds P . (Ug /\ b) = (P . Ug) * (P . b)
by A5, Th4;
let n be Element of NAT ; :: thesis: for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)

let b be Element of B; :: thesis: P . ((g . n) /\ b) = (P . (g . n)) * (P . b)

g . n in Indep (B,P)

end;let b be Element of B; :: thesis: P . ((g . n) /\ b) = (P . (g . n)) * (P . b)

g . n in Indep (B,P)

proof
end;

hence
P . ((g . n) /\ b) = (P . (g . n)) * (P . b)
by Def1; :: thesis: verumhence Union g in Indep (B,P) by Def1; :: thesis: verum

Z ` in Indep (B,P)

proof

then
Indp is Dynkin_System of Omega
by A2, A3, DYNKIN:def 5;
let Z be Subset of Omega; :: thesis: ( Z in Indep (B,P) implies Z ` in Indep (B,P) )

assume A6: Z in Indep (B,P) ; :: thesis: Z ` in Indep (B,P)

then reconsider Z = Z as Event of Sigma ;

reconsider Z9 = Z ` as Element of Sigma by PROB_1:20;

for b being Element of B holds P . ((Z `) /\ b) = (P . (Z `)) * (P . b)

hence Z ` in Indep (B,P) ; :: thesis: verum

end;assume A6: Z in Indep (B,P) ; :: thesis: Z ` in Indep (B,P)

then reconsider Z = Z as Event of Sigma ;

reconsider Z9 = Z ` as Element of Sigma by PROB_1:20;

for b being Element of B holds P . ((Z `) /\ b) = (P . (Z `)) * (P . b)

proof

then
Z9 in Indep (B,P)
by Def1;
let b be Element of B; :: thesis: P . ((Z `) /\ b) = (P . (Z `)) * (P . b)

P . (b /\ Z) = (P . b) * (P . Z) by A6, Def1;

then b,Z are_independent_respect_to P by PROB_2:def 4;

then b,([#] Sigma) \ Z are_independent_respect_to P by PROB_2:25;

hence P . ((Z `) /\ b) = (P . (Z `)) * (P . b) by PROB_2:def 4; :: thesis: verum

end;P . (b /\ Z) = (P . b) * (P . Z) by A6, Def1;

then b,Z are_independent_respect_to P by PROB_2:def 4;

then b,([#] Sigma) \ Z are_independent_respect_to P by PROB_2:25;

hence P . ((Z `) /\ b) = (P . (Z `)) * (P . b) by PROB_2:def 4; :: thesis: verum

hence Z ` in Indep (B,P) ; :: thesis: verum

hence Indep (B,P) is Dynkin_System of Omega ; :: thesis: verum