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

let Sigma be SigmaField of Omega; :: thesis: 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 )

let P be Probability of Sigma; :: thesis: 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 )

let A, B be non empty Subset of Sigma; :: thesis: ( 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 )

p,q are_independent_respect_to P ) by A1; :: thesis: verum

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 )

let Sigma be SigmaField of Omega; :: thesis: 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 )

let P be Probability of Sigma; :: thesis: 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 )

let A, B be non empty Subset of Sigma; :: thesis: ( 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 )

A1: now :: thesis: ( ( for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P ) implies A c= Indep (B,P) )

p,q are_independent_respect_to P ) implies A c= Indep (B,P) )

assume A2:
for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P ; :: thesis: A c= Indep (B,P)

thus A c= Indep (B,P) :: thesis: verum

end;p,q are_independent_respect_to P ; :: thesis: A c= Indep (B,P)

thus A c= Indep (B,P) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Indep (B,P) )

assume A3: x in A ; :: thesis: x in Indep (B,P)

then reconsider x = x as Event of Sigma ;

for b being Element of B holds P . (x /\ b) = (P . x) * (P . b) by A2, A3, PROB_2:def 4;

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

end;assume A3: x in A ; :: thesis: x in Indep (B,P)

then reconsider x = x as Event of Sigma ;

for b being Element of B holds P . (x /\ b) = (P . x) * (P . b) by A2, A3, PROB_2:def 4;

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

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

p,q are_independent_respect_to P )

hence
( 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 )

assume A4:
A c= Indep (B,P)
; :: thesis: for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P

thus for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P :: thesis: verum

end;p,q are_independent_respect_to P

thus for p, q being Event of Sigma st p in A & q in B holds

p,q are_independent_respect_to P :: thesis: verum

proof

let p, q be Event of Sigma; :: thesis: ( p in A & q in B implies p,q are_independent_respect_to P )

assume that

A5: p in A and

A6: q in B ; :: thesis: p,q are_independent_respect_to P

reconsider q = q as Element of B by A6;

reconsider p = p as Element of Sigma ;

P . (p /\ q) = (P . p) * (P . q) by A4, A5, Def1;

hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

end;assume that

A5: p in A and

A6: q in B ; :: thesis: p,q are_independent_respect_to P

reconsider q = q as Element of B by A6;

reconsider p = p as Element of Sigma ;

P . (p /\ q) = (P . p) * (P . q) by A4, A5, Def1;

hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

p,q are_independent_respect_to P ) by A1; :: thesis: verum