:: by Andrzej N\c{e}dzusiak

::

:: Received October 16, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th1: :: PROB_1:1

for r being real number

for seq being Real_Sequence st ex n being Element of NAT st

for m being Element of NAT st n <= m holds

seq . m = r holds

( seq is convergent & lim seq = r )

for seq being Real_Sequence st ex n being Element of NAT st

for m being Element of NAT st n <= m holds

seq . m = r holds

( seq is convergent & lim seq = r )

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 compl-closed means :Def1: :: PROB_1:def 1

for A being Subset of X st A in IT holds

A ` in IT;

for A being Subset of X st A in IT holds

A ` in IT;

:: deftheorem Def1 defines compl-closed PROB_1:def 1 :

for X being set

for IT being Subset-Family of X holds

( IT is compl-closed iff for A being Subset of X st A in IT holds

A ` in IT );

for X being set

for IT being Subset-Family of X holds

( IT is compl-closed iff for A being Subset of X st A in IT holds

A ` in IT );

registration
end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} = bool X holds

b_{1} is compl-closed

end;
coherence

for b

b

proof end;

registration

let X be set ;

existence

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

( not b_{1} is empty & b_{1} is compl-closed & b_{1} is cap-closed )

end;
existence

ex b

( not b

proof end;

definition
end;

theorem Th3: :: PROB_1:3

for X being set

for F being Field_Subset of X

for A, B being set st A in F & B in F holds

A \/ B in F

for F being Field_Subset of X

for A, B being set st A in F & B in F holds

A \/ B in F

proof end;

theorem Th6: :: PROB_1:6

for X being set

for F being Field_Subset of X

for A, B being Subset of X st A in F & B in F holds

A \ B in F

for F being Field_Subset of X

for A, B being Subset of X st A in F & B in F holds

A \ B in F

proof end;

theorem :: PROB_1:7

for X being set

for F being Field_Subset of X

for A, B being set st A in F & B in F holds

(A \ B) \/ B in F

for F being Field_Subset of X

for A, B being set st A in F & B in F holds

(A \ B) \/ B in F

proof end;

registration
end;

definition

let X be set ;

let A1 be SetSequence of X;

:: original: Union

redefine func Union A1 -> Subset of X;

coherence

Union A1 is Subset of X by Th11;

end;
let A1 be SetSequence of X;

:: original: Union

redefine func Union A1 -> Subset of X;

coherence

Union A1 is Subset of X by Th11;

theorem Th12: :: PROB_1:12

for X, x being set

for A1 being SetSequence of X holds

( x in Union A1 iff ex n being Element of NAT st x in A1 . n )

for A1 being SetSequence of X holds

( x in Union A1 iff ex n being Element of NAT st x in A1 . n )

proof end;

definition

let X be set ;

let A1 be SetSequence of X;

ex b_{1} being SetSequence of X st

for n being Element of NAT holds b_{1} . n = (A1 . n) `

for b_{1}, b_{2} being SetSequence of X st ( for n being Element of NAT holds b_{1} . n = (A1 . n) ` ) & ( for n being Element of NAT holds b_{2} . n = (A1 . n) ` ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being SetSequence of X st ( for n being Element of NAT holds b_{1} . n = (b_{2} . n) ` ) holds

for n being Element of NAT holds b_{2} . n = (b_{1} . n) `

end;
let A1 be SetSequence of X;

func Complement A1 -> SetSequence of X means :Def2: :: PROB_1:def 2

for n being Element of NAT holds it . n = (A1 . n) ` ;

existence for n being Element of NAT holds it . n = (A1 . n) ` ;

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

for n being Element of NAT holds b

proof end;

:: deftheorem Def2 defines Complement PROB_1:def 2 :

for X being set

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

( b_{3} = Complement A1 iff for n being Element of NAT holds b_{3} . n = (A1 . n) ` );

for X being set

for A1, b

( b

definition

let X be set ;

let A1 be SetSequence of X;

correctness

coherence

(Union (Complement A1)) ` is Subset of X;

;

end;
let A1 be SetSequence of X;

correctness

coherence

(Union (Complement A1)) ` is Subset of X;

;

:: deftheorem defines Intersection PROB_1:def 3 :

for X being set

for A1 being SetSequence of X holds Intersection A1 = (Union (Complement A1)) ` ;

for X being set

for A1 being SetSequence of X holds Intersection A1 = (Union (Complement A1)) ` ;

theorem Th13: :: PROB_1:13

for X, x being set

for A1 being SetSequence of X holds

( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )

for A1 being SetSequence of X holds

( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )

proof end;

Lm1: for X being set

for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)

proof end;

definition

let f be Function;

end;
attr f is non-ascending means :Def4: :: PROB_1:def 4

for n, m being Element of NAT st n <= m holds

f . m c= f . n;

for n, m being Element of NAT st n <= m holds

f . m c= f . n;

attr f is non-descending means :: PROB_1:def 5

for n, m being Element of NAT st n <= m holds

f . n c= f . m;

for n, m being Element of NAT st n <= m holds

f . n c= f . m;

:: deftheorem Def4 defines non-ascending PROB_1:def 4 :

for f being Function holds

( f is non-ascending iff for n, m being Element of NAT st n <= m holds

f . m c= f . n );

for f being Function holds

( f is non-ascending iff for n, m being Element of NAT st n <= m holds

f . m c= f . n );

:: deftheorem defines non-descending PROB_1:def 5 :

for f being Function holds

( f is non-descending iff for n, m being Element of NAT st n <= m holds

f . n c= f . m );

for f being Function holds

( f is non-descending iff for n, m being Element of NAT st n <= m holds

f . n c= f . m );

definition

let X be set ;

let F be Subset-Family of X;

end;
let F be Subset-Family of X;

attr F is sigma-multiplicative means :Def6: :: PROB_1:def 6

for A1 being SetSequence of X st rng A1 c= F holds

Intersection A1 in F;

for A1 being SetSequence of X st rng A1 c= F holds

Intersection A1 in F;

:: deftheorem Def6 defines sigma-multiplicative PROB_1:def 6 :

for X being set

for F being Subset-Family of X holds

( F is sigma-multiplicative iff for A1 being SetSequence of X st rng A1 c= F holds

Intersection A1 in F );

for X being set

for F being Subset-Family of X holds

( F is sigma-multiplicative iff for A1 being SetSequence of X st rng A1 c= F holds

Intersection A1 in F );

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} = bool X holds

b_{1} is sigma-multiplicative

end;
coherence

for b

b

proof end;

registration

let X be set ;

existence

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

( b_{1} is compl-closed & b_{1} is sigma-multiplicative & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition

let X be set ;

mode SigmaField of X is non empty compl-closed sigma-multiplicative Subset-Family of X;

end;
mode SigmaField of X is non empty compl-closed sigma-multiplicative Subset-Family of X;

theorem :: PROB_1:15

registration

let X be set ;

coherence

for b_{1} being SigmaField of X holds

( b_{1} is cap-closed & b_{1} is compl-closed )
by Th16;

end;
coherence

for b

( b

:: sequences of elements of given sigma-field (subsets of given nonempty set

:: Omega) Sigma are introduced; also notion of Event from this sigma-field is

:: introduced; then some previous theorems are reformulated in language of

:: these notions.

:: Omega) Sigma are introduced; also notion of Event from this sigma-field is

:: introduced; then some previous theorems are reformulated in language of

:: these notions.

registration

let X be set ;

let F be non empty Subset-Family of X;

ex b_{1} being SetSequence of X st b_{1} is F -valued

end;
let F be non empty Subset-Family of X;

cluster Relation-like NAT -defined F -valued bool X -valued Function-like V37( NAT , bool X) for Event of ;

existence ex b

proof end;

definition

let X be set ;

let F be non empty Subset-Family of X;

mode SetSequence of F is F -valued SetSequence of X;

end;
let F be non empty Subset-Family of X;

mode SetSequence of F is F -valued SetSequence of X;

theorem Th17: :: PROB_1:17

for X being set

for Si being SigmaField of X

for ASeq being SetSequence of Si holds Union ASeq in Si

for Si being SigmaField of X

for ASeq being SetSequence of Si holds Union ASeq in Si

proof end;

definition

let X be set ;

let F be SigmaField of X;

:: original: Event

redefine mode Event of F -> Subset of X;

coherence

for b_{1} being Event of holds b_{1} is Subset of X

end;
let F be SigmaField of X;

:: original: Event

redefine mode Event of F -> Subset of X;

coherence

for b

proof end;

theorem :: PROB_1:18

theorem :: PROB_1:19

for X being set

for Si being SigmaField of X

for A, B being Event of Si holds A /\ B is Event of Si by FINSUB_1:def 2;

for Si being SigmaField of X

for A, B being Event of Si holds A /\ B is Event of Si by FINSUB_1:def 2;

theorem :: PROB_1:20

theorem :: PROB_1:21

theorem :: PROB_1:24

registration

let X be set ;

let Si be SigmaField of X;

existence

ex b_{1} being Event of Si st b_{1} is empty

end;
let Si be SigmaField of X;

existence

ex b

proof end;

:: deftheorem defines [#] PROB_1:def 7 :

for X being set

for Si being SigmaField of X holds [#] Si = X;

for X being set

for Si being SigmaField of X holds [#] Si = X;

definition

let X be set ;

let Si be SigmaField of X;

let A, B be Event of Si;

:: original: /\

redefine func A /\ B -> Event of Si;

coherence

A /\ B is Event of Si by FINSUB_1:def 2;

:: original: \/

redefine func A \/ B -> Event of Si;

coherence

A \/ B is Event of Si by Th3;

:: original: \

redefine func A \ B -> Event of Si;

coherence

A \ B is Event of Si by Th6;

end;
let Si be SigmaField of X;

let A, B be Event of Si;

:: original: /\

redefine func A /\ B -> Event of Si;

coherence

A /\ B is Event of Si by FINSUB_1:def 2;

:: original: \/

redefine func A \/ B -> Event of Si;

coherence

A \/ B is Event of Si by Th3;

:: original: \

redefine func A \ B -> Event of Si;

coherence

A \ B is Event of Si by Th6;

theorem :: PROB_1:25

for X being set

for A1 being SetSequence of X

for Si being SigmaField of X holds

( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )

for A1 being SetSequence of X

for Si being SigmaField of X holds

( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )

proof end;

theorem :: PROB_1:26

for Omega being set

for ASeq being SetSequence of Omega

for Sigma being SigmaField of Omega st ASeq is SetSequence of Sigma holds

Union ASeq is Event of Sigma by Th17;

for ASeq being SetSequence of Omega

for Sigma being SigmaField of Omega st ASeq is SetSequence of Sigma holds

Union ASeq is Event of Sigma by Th17;

theorem Th27: :: PROB_1:27

for Omega, p being set

for Sigma being SigmaField of Omega ex f being Function st

( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds

( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )

for Sigma being SigmaField of Omega ex f being Function st

( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds

( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )

proof end;

theorem Th28: :: PROB_1:28

for Omega, p being set

for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st

for D being Subset of Omega st D in Sigma holds

( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )

for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st

for D being Subset of Omega st D in Sigma holds

( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )

proof end;

theorem Th29: :: PROB_1:29

for Omega being set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence

proof end;

definition

let Omega be set ;

let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

let P be Function of Sigma,REAL;

:: original: *

redefine func P * ASeq -> Real_Sequence;

coherence

ASeq * P is Real_Sequence by Th29;

end;
let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

let P be Function of Sigma,REAL;

:: original: *

redefine func P * ASeq -> Real_Sequence;

coherence

ASeq * P is Real_Sequence by Th29;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

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

( ( for A being Event of Sigma holds 0 <= b_{1} . A ) & b_{1} . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

b_{1} . (A \/ B) = (b_{1} . A) + (b_{1} . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( b_{1} * ASeq is convergent & lim (b_{1} * ASeq) = b_{1} . (Intersection ASeq) ) ) )

end;
let Sigma be SigmaField of Omega;

mode Probability of Sigma -> Function of Sigma,REAL means :Def8: :: PROB_1:def 8

( ( for A being Event of Sigma holds 0 <= it . A ) & it . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

it . (A \/ B) = (it . A) + (it . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( it * ASeq is convergent & lim (it * ASeq) = it . (Intersection ASeq) ) ) );

existence ( ( for A being Event of Sigma holds 0 <= it . A ) & it . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

it . (A \/ B) = (it . A) + (it . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( it * ASeq is convergent & lim (it * ASeq) = it . (Intersection ASeq) ) ) );

ex b

( ( for A being Event of Sigma holds 0 <= b

b

( b

proof end;

:: deftheorem Def8 defines Probability PROB_1:def 8 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for b_{3} being Function of Sigma,REAL holds

( b_{3} is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b_{3} . A ) & b_{3} . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

b_{3} . (A \/ B) = (b_{3} . A) + (b_{3} . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds

( b_{3} * ASeq is convergent & lim (b_{3} * ASeq) = b_{3} . (Intersection ASeq) ) ) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for b

( b

b

( b

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

coherence

for b_{1} being Probability of Sigma holds b_{1} is zeroed

end;
let Sigma be SigmaField of Omega;

coherence

for b

proof end;

theorem :: PROB_1:30

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma holds P . ([#] Sigma) = 1 by Def8;

for Sigma being SigmaField of Omega

for P being Probability of Sigma holds P . ([#] Sigma) = 1 by Def8;

theorem Th31: :: PROB_1:31

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1

proof end;

theorem :: PROB_1:32

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

proof end;

theorem Th33: :: PROB_1:33

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . (B \ A) = (P . B) - (P . A)

proof end;

theorem Th34: :: PROB_1:34

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . A <= P . B

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . A <= P . B

proof end;

theorem :: PROB_1:35

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds P . A <= 1

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds P . A <= 1

proof end;

theorem Th36: :: PROB_1:36

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))

proof end;

theorem Th37: :: PROB_1:37

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))

proof end;

theorem Th38: :: PROB_1:38

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))

proof end;

theorem :: PROB_1:39

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)

proof end;

definition

let Omega be non empty set ;

let X be Subset-Family of Omega;

ex b_{1} being SigmaField of Omega st

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

b_{1} c= Z ) )

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

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

b_{2} c= Z ) holds

b_{1} = b_{2}

end;
let X be Subset-Family of Omega;

func sigma X -> SigmaField of Omega means :: PROB_1:def 9

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

it c= Z ) );

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

it c= Z ) );

ex b

( X c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines sigma PROB_1:def 9 :

for Omega being non empty set

for X being Subset-Family of Omega

for b_{3} being SigmaField of Omega holds

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

b_{3} c= Z ) ) );

for Omega being non empty set

for X being Subset-Family of Omega

for b

( b

b

:: deftheorem defines halfline PROB_1:def 10 :

for r being ext-real number holds halfline r = ].-infty,r.[;

for r being ext-real number holds halfline r = ].-infty,r.[;

definition

{ (halfline r) where r is Element of REAL : verum } is Subset-Family of REAL
end;

func Family_of_halflines -> Subset-Family of REAL equals :: PROB_1:def 11

{ (halfline r) where r is Element of REAL : verum } ;

coherence { (halfline r) where r is Element of REAL : verum } ;

{ (halfline r) where r is Element of REAL : verum } is Subset-Family of REAL

proof end;

:: deftheorem defines Family_of_halflines PROB_1:def 11 :

Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ;

Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ;

theorem :: PROB_1:41

for X being set

for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;

for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;

definition

let X, Y be set ;

let A be Subset-Family of X;

let F be Function of Y,(bool A);

let x be set ;

:: original: .

redefine func F . x -> Subset-Family of X;

coherence

F . x is Subset-Family of X

end;
let A be Subset-Family of X;

let F be Function of Y,(bool A);

let x be set ;

:: original: .

redefine func F . x -> Subset-Family of X;

coherence

F . x is Subset-Family of X

proof end;

:: a field of subsets of given nonempty set Omega. ::