:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received August 12, 2005

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

Lm1: for t, p, s being Real st 0 < s & t <= p holds

( t < p + s & t - s < p )

proof end;

theorem Th3: :: PROB_3:3

for g being Real

for f being Real_Sequence st ex k being Nat st

for n being Nat st k <= n holds

f . n = g holds

( f is convergent & lim f = g )

for f being Real_Sequence st ex k being Nat st

for n being Nat st k <= n holds

f . n = g holds

( f is convergent & lim f = g )

proof end;

theorem Th4: :: PROB_3:4

for n being Nat

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

proof end;

theorem Th5: :: PROB_3:5

for n being Nat

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

proof end;

theorem Th6: :: PROB_3:6

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V75() holds

P * ASeq is non-decreasing

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V75() holds

P * ASeq is non-decreasing

proof end;

theorem Th7: :: PROB_3:7

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

proof end;

definition

let X be set ;

let A1 be SetSequence of X;

ex b_{1} being SetSequence of X st

( b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) /\ (A1 . (n + 1)) ) )

for b_{1}, b_{2} being SetSequence of X st b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) /\ (A1 . (n + 1)) ) & b_{2} . 0 = A1 . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) /\ (A1 . (n + 1)) ) holds

b_{1} = b_{2}

end;
let A1 be SetSequence of X;

func Partial_Intersection A1 -> SetSequence of X means :Def1: :: PROB_3:def 1

( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) /\ (A1 . (n + 1)) ) );

existence ( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) /\ (A1 . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :

for X being set

for A1, b_{3} being SetSequence of X holds

( b_{3} = Partial_Intersection A1 iff ( b_{3} . 0 = A1 . 0 & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) /\ (A1 . (n + 1)) ) ) );

for X being set

for A1, b

( b

definition

let X be set ;

let A1 be SetSequence of X;

ex b_{1} being SetSequence of X st

( b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ (A1 . (n + 1)) ) )

for b_{1}, b_{2} being SetSequence of X st b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ (A1 . (n + 1)) ) & b_{2} . 0 = A1 . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) \/ (A1 . (n + 1)) ) holds

b_{1} = b_{2}

end;
let A1 be SetSequence of X;

func Partial_Union A1 -> SetSequence of X means :Def2: :: PROB_3:def 2

( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ (A1 . (n + 1)) ) );

existence ( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ (A1 . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :

for X being set

for A1, b_{3} being SetSequence of X holds

( b_{3} = Partial_Union A1 iff ( b_{3} . 0 = A1 . 0 & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) \/ (A1 . (n + 1)) ) ) );

for X being set

for A1, b

( b

theorem Th8: :: PROB_3:8

for n being Nat

for X being set

for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n

for X being set

for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n

proof end;

theorem Th9: :: PROB_3:9

for n being Nat

for X being set

for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

for X being set

for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

proof end;

theorem Th12: :: PROB_3:12

for n being Nat

for X being set

for A1 being SetSequence of X

for x being object holds

( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds

x in A1 . k )

for X being set

for A1 being SetSequence of X

for x being object holds

( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds

x in A1 . k )

proof end;

theorem Th13: :: PROB_3:13

for n being Nat

for x being object

for X being set

for A1 being SetSequence of X holds

( x in (Partial_Union A1) . n iff ex k being Nat st

( k <= n & x in A1 . k ) )

for x being object

for X being set

for A1 being SetSequence of X holds

( x in (Partial_Union A1) . n iff ex k being Nat st

( k <= n & x in A1 . k ) )

proof end;

theorem Th14: :: PROB_3:14

for X being set

for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1

for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1

proof end;

definition

let X be set ;

let A1 be SetSequence of X;

ex b_{1} being SetSequence of X st

( b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )

for b_{1}, b_{2} being SetSequence of X st b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) & b_{2} . 0 = A1 . 0 & ( for n being Nat holds b_{2} . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) holds

b_{1} = b_{2}

end;
let A1 be SetSequence of X;

func Partial_Diff_Union A1 -> SetSequence of X means :Def3: :: PROB_3:def 3

( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) );

existence ( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :

for X being set

for A1, b_{3} being SetSequence of X holds

( b_{3} = Partial_Diff_Union A1 iff ( b_{3} . 0 = A1 . 0 & ( for n being Nat holds b_{3} . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) );

for X being set

for A1, b

( b

theorem Th16: :: PROB_3:16

for n being Nat

for x being object

for X being set

for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

for x being object

for X being set

for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

proof end;

theorem Th17: :: PROB_3:17

for n being Nat

for X being set

for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n by Th16;

for X being set

for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n by Th16;

theorem Th18: :: PROB_3:18

for n being Nat

for X being set

for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n

for X being set

for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n

proof end;

theorem Th19: :: PROB_3:19

for X being set

for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1

for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1

proof end;

definition

let X be set ;

let A1 be SetSequence of X;

( A1 is disjoint_valued iff for m, n being Nat st m <> n holds

A1 . m misses A1 . n )

end;
let A1 be SetSequence of X;

:: original: disjoint_valued

redefine attr A1 is disjoint_valued means :: PROB_3:def 4

for m, n being Nat st m <> n holds

A1 . m misses A1 . n;

compatibility redefine attr A1 is disjoint_valued means :: PROB_3:def 4

for m, n being Nat st m <> n holds

A1 . m misses A1 . n;

( A1 is disjoint_valued iff for m, n being Nat st m <> n holds

A1 . m misses A1 . n )

proof end;

:: deftheorem defines disjoint_valued PROB_3:def 4 :

for X being set

for A1 being SetSequence of X holds

( A1 is disjoint_valued iff for m, n being Nat st m <> n holds

A1 . m misses A1 . n );

for X being set

for A1 being SetSequence of X holds

( A1 is disjoint_valued iff for m, n being Nat st m <> n holds

A1 . m misses A1 . n );

registration

let X be set ;

let A1 be SetSequence of X;

coherence

Partial_Diff_Union A1 is disjoint_valued

end;
let A1 be SetSequence of X;

coherence

Partial_Diff_Union A1 is disjoint_valued

proof end;

registration

let X be set ;

let Si be SigmaField of X;

let XSeq be SetSequence of Si;

coherence

Partial_Intersection XSeq is Si -valued

end;
let Si be SigmaField of X;

let XSeq be SetSequence of Si;

coherence

Partial_Intersection XSeq is Si -valued

proof end;

registration

let X be set ;

let Si be SigmaField of X;

let XSeq be SetSequence of Si;

coherence

Partial_Union XSeq is Si -valued

end;
let Si be SigmaField of X;

let XSeq be SetSequence of Si;

coherence

Partial_Union XSeq is Si -valued

proof end;

registration

let X be set ;

let Si be SigmaField of X;

let XSeq be SetSequence of Si;

coherence

Partial_Diff_Union XSeq is Si -valued

end;
let Si be SigmaField of X;

let XSeq be SetSequence of Si;

coherence

Partial_Diff_Union XSeq is Si -valued

proof end;

theorem :: PROB_3:21

theorem :: PROB_3:22

theorem :: PROB_3:23

for n being Nat

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds (Partial_Intersection XSeq) . n c= XSeq . n by Th8;

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds (Partial_Intersection XSeq) . n c= XSeq . n by Th8;

theorem :: PROB_3:24

for n being Nat

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds XSeq . n c= (Partial_Union XSeq) . n by Th9;

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds XSeq . n c= (Partial_Union XSeq) . n by Th9;

theorem :: PROB_3:25

for n being Nat

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si

for x being object holds

( x in (Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds

x in XSeq . k )

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si

for x being object holds

( x in (Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds

x in XSeq . k )

proof end;

theorem :: PROB_3:26

for n being Nat

for x being object

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds

( x in (Partial_Union XSeq) . n iff ex k being Nat st

( k <= n & x in XSeq . k ) )

for x being object

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds

( x in (Partial_Union XSeq) . n iff ex k being Nat st

( k <= n & x in XSeq . k ) )

proof end;

theorem :: PROB_3:27

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Partial_Intersection XSeq is V74() by Th10;

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Partial_Intersection XSeq is V74() by Th10;

theorem :: PROB_3:28

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Partial_Union XSeq is V75() by Th11;

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Partial_Union XSeq is V75() by Th11;

theorem :: PROB_3:29

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Intersection (Partial_Intersection XSeq) = Intersection XSeq by Th14;

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Intersection (Partial_Intersection XSeq) = Intersection XSeq by Th14;

theorem :: PROB_3:30

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Union (Partial_Union XSeq) = Union XSeq by Th15;

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Union (Partial_Union XSeq) = Union XSeq by Th15;

theorem :: PROB_3:31

for X being set

for Si being SigmaField of X

for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Diff_Union XSeq holds

( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (XSeq . (n + 1)) \ ((Partial_Union XSeq) . n) ) ) by Def3;

for Si being SigmaField of X

for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Diff_Union XSeq holds

( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (XSeq . (n + 1)) \ ((Partial_Union XSeq) . n) ) ) by Def3;

theorem :: PROB_3:32

for n being Nat

for x being object

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

for x being object

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

proof end;

theorem :: PROB_3:33

for n being Nat

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= XSeq . n by Th17;

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= XSeq . n by Th17;

theorem :: PROB_3:34

for n being Nat

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= (Partial_Union XSeq) . n by Th18;

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= (Partial_Union XSeq) . n by Th18;

theorem :: PROB_3:35

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19;

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19;

theorem :: PROB_3:36

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Union (Partial_Diff_Union XSeq) = Union XSeq by Th20;

for Si being SigmaField of X

for XSeq being SetSequence of Si holds Union (Partial_Diff_Union XSeq) = Union XSeq by Th20;

theorem Th37: :: PROB_3:37

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing

proof end;

theorem :: PROB_3:38

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

proof end;

theorem :: PROB_3:39

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

proof end;

theorem Th40: :: PROB_3:40

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

proof end;

theorem Th41: :: PROB_3:41

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds

( P * (Partial_Union ASeq) is convergent & lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) & lim (P * (Partial_Union ASeq)) = P . (Union ASeq) )

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds

( P * (Partial_Union ASeq) is convergent & lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) & lim (P * (Partial_Union ASeq)) = P . (Union ASeq) )

proof end;

theorem Th42: :: PROB_3:42

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma st ASeq is V77() holds

for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma st ASeq is V77() holds

for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

proof end;

theorem Th43: :: PROB_3:43

for n being Nat

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

proof end;

theorem Th44: :: PROB_3:44

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th43;

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th43;

theorem Th45: :: PROB_3:45

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

proof end;

theorem Th46: :: PROB_3:46

for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

proof end;

definition

let X be set ;

let F1 be FinSequence of bool X;

let n be Nat;

:: original: .

redefine func F1 . n -> Subset of X;

coherence

F1 . n is Subset of X

end;
let F1 be FinSequence of bool X;

let n be Nat;

:: original: .

redefine func F1 . n -> Subset of X;

coherence

F1 . n is Subset of X

proof end;

theorem :: PROB_3:47

for X being set ex F1 being FinSequence of bool X st

for k being Nat st k in dom F1 holds

F1 . k = X

for k being Nat st k in dom F1 holds

F1 . k = X

proof end;

theorem :: PROB_3:48

definition

let X be set ;

let F1 be FinSequence of bool X;

:: original: Union

redefine func Union F1 -> Subset of X;

coherence

Union F1 is Subset of X

end;
let F1 be FinSequence of bool X;

:: original: Union

redefine func Union F1 -> Subset of X;

coherence

Union F1 is Subset of X

proof end;

theorem Th49: :: PROB_3:49

for x being object

for X being set

for F1 being FinSequence of bool X holds

( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

for X being set

for F1 being FinSequence of bool X holds

( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

proof end;

definition

let X be set ;

let F1 be FinSequence of bool X;

ex b_{1} being FinSequence of bool X st

( len b_{1} = len F1 & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (F1 . n) ` ) )

for b_{1}, b_{2} being FinSequence of bool X st len b_{1} = len F1 & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (F1 . n) ` ) & len b_{2} = len F1 & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = (F1 . n) ` ) holds

b_{1} = b_{2}

end;
let F1 be FinSequence of bool X;

func Complement F1 -> FinSequence of bool X means :Def5: :: PROB_3:def 5

( len it = len F1 & ( for n being Nat st n in dom it holds

it . n = (F1 . n) ` ) );

existence ( len it = len F1 & ( for n being Nat st n in dom it holds

it . n = (F1 . n) ` ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines Complement PROB_3:def 5 :

for X being set

for F1, b_{3} being FinSequence of bool X holds

( b_{3} = Complement F1 iff ( len b_{3} = len F1 & ( for n being Nat st n in dom b_{3} holds

b_{3} . n = (F1 . n) ` ) ) );

for X being set

for F1, b

( b

b

definition

let X be set ;

let F1 be FinSequence of bool X;

( ( F1 <> {} implies (Union (Complement F1)) ` is Subset of X ) & ( not F1 <> {} implies {} is Subset of X ) ) by SUBSET_1:1;

consistency

for b_{1} being Subset of X holds verum
;

end;
let F1 be FinSequence of bool X;

func Intersection F1 -> Subset of X equals :Def6: :: PROB_3:def 6

(Union (Complement F1)) ` if F1 <> {}

otherwise {} ;

coherence (Union (Complement F1)) ` if F1 <> {}

otherwise {} ;

( ( F1 <> {} implies (Union (Complement F1)) ` is Subset of X ) & ( not F1 <> {} implies {} is Subset of X ) ) by SUBSET_1:1;

consistency

for b

:: deftheorem Def6 defines Intersection PROB_3:def 6 :

for X being set

for F1 being FinSequence of bool X holds

( ( F1 <> {} implies Intersection F1 = (Union (Complement F1)) ` ) & ( not F1 <> {} implies Intersection F1 = {} ) );

for X being set

for F1 being FinSequence of bool X holds

( ( F1 <> {} implies Intersection F1 = (Union (Complement F1)) ` ) & ( not F1 <> {} implies Intersection F1 = {} ) );

theorem Th51: :: PROB_3:51

for X being set

for F1 being FinSequence of bool X

for x being object st F1 <> {} holds

( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k )

for F1 being FinSequence of bool X

for x being object st F1 <> {} holds

( x in Intersection F1 iff for k being Nat st k in dom F1 holds

x in F1 . k )

proof end;

theorem Th52: :: PROB_3:52

for x being object

for X being set

for F1 being FinSequence of bool X st F1 <> {} holds

( x in meet (rng F1) iff for n being Nat st n in dom F1 holds

x in F1 . n )

for X being set

for F1 being FinSequence of bool X st F1 <> {} holds

( x in meet (rng F1) iff for n being Nat st n in dom F1 holds

x in F1 . n )

proof end;

theorem Th54: :: PROB_3:54

for X being set

for F1 being FinSequence of bool X ex A1 being SetSequence of X st

( ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) )

for F1 being FinSequence of bool X ex A1 being SetSequence of X st

( ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) )

proof end;

theorem Th55: :: PROB_3:55

for X being set

for F1 being FinSequence of bool X

for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) holds

( A1 . 0 = {} & Union A1 = Union F1 )

for F1 being FinSequence of bool X

for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) holds

( A1 . 0 = {} & Union A1 = Union F1 )

proof end;

definition

let X be set ;

let Si be SigmaField of X;

:: original: FinSequence

redefine mode FinSequence of Si -> FinSequence of bool X;

coherence

for b_{1} being FinSequence of Si holds b_{1} is FinSequence of bool X

end;
let Si be SigmaField of X;

:: original: FinSequence

redefine mode FinSequence of Si -> FinSequence of bool X;

coherence

for b

proof end;

definition

let X be set ;

let Si be SigmaField of X;

let FSi be FinSequence of Si;

let n be Nat;

:: original: .

redefine func FSi . n -> Event of Si;

coherence

FSi . n is Event of Si

end;
let Si be SigmaField of X;

let FSi be FinSequence of Si;

let n be Nat;

:: original: .

redefine func FSi . n -> Event of Si;

coherence

FSi . n is Event of Si

proof end;

theorem Th56: :: PROB_3:56

for X being set

for Si being SigmaField of X

for FSi being FinSequence of Si ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

for Si being SigmaField of X

for FSi being FinSequence of Si ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

proof end;

registration

let X be set ;

let S be SigmaField of X;

let F be FinSequence of S;

coherence

Complement F is S -valued

end;
let S be SigmaField of X;

let F be FinSequence of S;

coherence

Complement F is S -valued

proof end;

theorem :: PROB_3:58

for X being set

for Si being SigmaField of X

for FSi being FinSequence of Si holds Intersection FSi in Si

for Si being SigmaField of X

for FSi being FinSequence of Si holds Intersection FSi in Si

proof end;

theorem Th59: :: PROB_3:59

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

proof end;

theorem Th60: :: PROB_3:60

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let FSeq be FinSequence of Sigma;

let P be Probability of Sigma;

:: original: *

redefine func P * FSeq -> FinSequence of REAL ;

coherence

FSeq * P is FinSequence of REAL by Th60;

end;
let Sigma be SigmaField of Omega;

let FSeq be FinSequence of Sigma;

let P be Probability of Sigma;

:: original: *

redefine func P * FSeq -> FinSequence of REAL ;

coherence

FSeq * P is FinSequence of REAL by Th60;

theorem Th61: :: PROB_3:61

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

proof end;

theorem Th63: :: PROB_3:63

for RFin being FinSequence of REAL st len RFin >= 1 holds

ex f being Real_Sequence st

( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds

f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) )

ex f being Real_Sequence st

( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds

f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) )

proof end;

theorem Th64: :: PROB_3:64

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma

for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds

ASeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds

ASeq . k = {} ) holds

( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) & P . (Union ASeq) <= Sum (P * ASeq) & Sum (P * FSeq) = Sum (P * ASeq) )

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma

for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds

ASeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds

ASeq . k = {} ) holds

( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) & P . (Union ASeq) <= Sum (P * ASeq) & Sum (P * FSeq) = Sum (P * ASeq) )

proof end;

theorem :: PROB_3:65

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds

( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds

( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )

proof end;

definition

let X be set ;

let IT be Subset-Family of X;

end;
let IT be Subset-Family of X;

attr IT is non-decreasing-closed means :Def7: :: PROB_3:def 9

for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds

Union A1 in IT;

for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds

Union A1 in IT;

attr IT is non-increasing-closed means :Def8: :: PROB_3:def 10

for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

Intersection A1 in IT;

for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

Intersection A1 in IT;

:: deftheorem Def7 defines non-decreasing-closed PROB_3:def 9 :

for X being set

for IT being Subset-Family of X holds

( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds

Union A1 in IT );

for X being set

for IT being Subset-Family of X holds

( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds

Union A1 in IT );

:: deftheorem Def8 defines non-increasing-closed PROB_3:def 10 :

for X being set

for IT being Subset-Family of X holds

( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

Intersection A1 in IT );

for X being set

for IT being Subset-Family of X holds

( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

Intersection A1 in IT );

theorem Th66: :: PROB_3:66

for X being set

for IT being Subset-Family of X holds

( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds

lim A1 in IT )

for IT being Subset-Family of X holds

( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds

lim A1 in IT )

proof end;

theorem Th67: :: PROB_3:67

for X being set

for IT being Subset-Family of X holds

( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT )

for IT being Subset-Family of X holds

( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT )

proof end;

registration

let X be set ;

existence

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

( b_{1} is non-decreasing-closed & b_{1} is non-increasing-closed )

end;
existence

ex b

( b

proof end;

definition

let X be set ;

mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X;

end;
mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X;

theorem Th69: :: PROB_3:69

for X, Z being set holds

( Z is MonotoneClass of X iff ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds

lim A1 in Z ) ) )

( Z is MonotoneClass of X iff ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds

lim A1 in Z ) ) )

proof end;

theorem Th70: :: PROB_3:70

for X being set

for F being Field_Subset of X holds

( F is SigmaField of X iff F is MonotoneClass of X )

for F being Field_Subset of X holds

( F is SigmaField of X iff F is MonotoneClass of X )

proof end;

theorem :: PROB_3:71

definition

let Omega be non empty set ;

let X be Subset-Family of Omega;

ex b_{1} being MonotoneClass of Omega st

( X c= b_{1} & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds

b_{1} c= Z ) )

for b_{1}, b_{2} being MonotoneClass of Omega st X c= b_{1} & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds

b_{1} c= Z ) & X c= b_{2} & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds

b_{2} c= Z ) holds

b_{1} = b_{2}
;

end;
let X be Subset-Family of Omega;

func monotoneclass X -> MonotoneClass of Omega means :Def9: :: PROB_3:def 11

( X c= it & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds

it c= Z ) );

existence ( X c= it & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds

it c= Z ) );

ex b

( X c= b

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def9 defines monotoneclass PROB_3:def 11 :

for Omega being non empty set

for X being Subset-Family of Omega

for b_{3} being MonotoneClass of Omega holds

( b_{3} = monotoneclass X iff ( X c= b_{3} & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds

b_{3} c= Z ) ) );

for Omega being non empty set

for X being Subset-Family of Omega

for b

( b

b

theorem Th72: :: PROB_3:72

for Omega being non empty set

for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega

for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega

proof end;