:: by Andrzej N\c{e}dzusiak

::

:: Received October 16, 1989

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

begin

theorem :: PROB_1:1

canceled;

theorem :: PROB_1:2

canceled;

theorem Th3: :: PROB_1:3 [edit]

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;

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;

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;

:: 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 );

registration
end;

registration

let X be set ;

cluster bool X -> compl-closed Subset-Family of X;

coherence

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

b_{1} is compl-closed

end;
cluster bool X -> compl-closed Subset-Family of X;

coherence

for b

b

proof end;

registration

let X be set ;

cluster non empty cap-closed compl-closed Event of ;

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;
cluster non empty cap-closed compl-closed Event of ;

existence

ex b

( not b

proof end;

definition
end;

theorem Th4: :: PROB_1:4 [edit]

proof end;

theorem :: PROB_1:5

canceled;

theorem :: PROB_1:6

canceled;

theorem :: PROB_1:7

canceled;

theorem :: PROB_1:8

canceled;

theorem Th9: :: PROB_1:9 [edit]

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 Th10: :: PROB_1:10 [edit]

proof end;

theorem Th11: :: PROB_1:11 [edit]

proof end;

theorem Th12: :: PROB_1:12 [edit]

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:13 [edit]

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;

theorem :: PROB_1:14 [edit]

proof end;

theorem :: PROB_1:15 [edit]

theorem :: PROB_1:16 [edit]

proof end;

theorem :: PROB_1:17

canceled;

theorem :: PROB_1:18 [edit]

proof end;

theorem :: PROB_1:19

canceled;

theorem :: PROB_1:20

canceled;

theorem :: PROB_1:21

canceled;

theorem :: PROB_1:22

canceled;

theorem Th23: :: PROB_1:23 [edit]

proof 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 Th23;

end;
let A1 be SetSequence of X;

:: original: Union

redefine func Union A1 -> Subset of X;

coherence

Union A1 is Subset of X by Th23;

theorem :: PROB_1:24

canceled;

theorem Th25: :: PROB_1:25 [edit]

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;

theorem Th26: :: PROB_1:26 [edit]

for X being set

for A1 being SetSequence of X ex B1 being SetSequence of X st

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

for A1 being SetSequence of X ex B1 being SetSequence of X st

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

proof end;

definition

let X be set ;

let A1 be SetSequence of X;

canceled;

canceled;

func Complement A1 -> SetSequence of X means :Def4: :: PROB_1:def 4

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

existence

ex b_{1} being SetSequence of X st

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

uniqueness

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;

canceled;

canceled;

func Complement A1 -> SetSequence of X means :Def4: :: PROB_1:def 4

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

existence

ex b

for n being Element of NAT holds b

uniqueness

for b

b

proof end;

involutiveness for b

for n being Element of NAT holds b

proof end;

:: deftheorem PROB_1:def 2 :

canceled;

:: deftheorem PROB_1:def 3 :

canceled;

:: deftheorem Def4 defines Complement PROB_1:def 4 :

for X being set

for A1, b

( b

definition

let X be set ;

let A1 be SetSequence of X;

func Intersection A1 -> Subset of X equals :: PROB_1:def 5

(Union (Complement A1)) ` ;

correctness

coherence

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

;

end;
let A1 be SetSequence of X;

func Intersection A1 -> Subset of X equals :: PROB_1:def 5

(Union (Complement A1)) ` ;

correctness

coherence

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

;

:: deftheorem defines Intersection PROB_1:def 5 :

for X being set

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

theorem :: PROB_1:27

canceled;

theorem :: PROB_1:28

canceled;

theorem Th29: :: PROB_1:29 [edit]

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;

Lm2: for X being set

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

proof end;

theorem Th30: :: PROB_1:30 [edit]

proof end;

definition

let f be Function;

attr f is non-ascending means :Def6: :: PROB_1:def 6

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 7

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

f . n c= f . m;

end;
attr f is non-ascending means :Def6: :: PROB_1:def 6

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 7

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

f . n c= f . m;

:: deftheorem Def6 defines non-ascending PROB_1:def 6 :

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 7 :

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;

attr F is sigma-multiplicative means :Def8: :: PROB_1:def 8

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

Intersection A1 in F;

end;
let F be Subset-Family of X;

attr F is sigma-multiplicative means :Def8: :: PROB_1:def 8

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

Intersection A1 in F;

:: deftheorem Def8 defines sigma-multiplicative PROB_1:def 8 :

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 ;

cluster bool X -> sigma-multiplicative Subset-Family of X;

coherence

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

b_{1} is sigma-multiplicative

end;
cluster bool X -> sigma-multiplicative Subset-Family of X;

coherence

for b

b

proof end;

registration

let X be set ;

cluster non empty compl-closed sigma-multiplicative Event of ;

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;
cluster non empty compl-closed sigma-multiplicative Event of ;

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:31

canceled;

theorem :: PROB_1:32 [edit]

for X being set

for S being non empty set holds

( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds

Intersection A1 in S ) & ( for A being Subset of X st A in S holds

A ` in S ) ) ) by Def1, Def8;

for S being non empty set holds

( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds

Intersection A1 in S ) & ( for A being Subset of X st A in S holds

A ` in S ) ) ) by Def1, Def8;

theorem :: PROB_1:33

canceled;

theorem :: PROB_1:34

canceled;

theorem Th35: :: PROB_1:35 [edit]

proof end;

registration

let X be set ;

cluster non empty compl-closed sigma-multiplicative -> cap-closed Event of ;

coherence

for b_{1} being SigmaField of X holds

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

end;
cluster non empty compl-closed sigma-multiplicative -> cap-closed Event of ;

coherence

for b

( b

registration

let X be set ;

let Si be SigmaField of X;

cluster Relation-like NAT -defined Si -valued bool X -valued Function-like V34( NAT , bool X) Event of ;

existence

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

end;
let Si be SigmaField of X;

cluster Relation-like NAT -defined Si -valued bool X -valued Function-like V34( NAT , bool X) Event of ;

existence

ex b

proof end;

definition
end;

theorem :: PROB_1:36

canceled;

theorem :: PROB_1:37

canceled;

theorem :: PROB_1:38

canceled;

theorem :: PROB_1:39

canceled;

theorem :: PROB_1:40

canceled;

theorem :: PROB_1:41

canceled;

theorem :: PROB_1:42

canceled;

theorem :: PROB_1:43

canceled;

theorem :: PROB_1:44

canceled;

theorem :: PROB_1:45

canceled;

theorem Th46: :: PROB_1:46 [edit]

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:47

canceled;

theorem :: PROB_1:48 [edit]

theorem :: PROB_1:49 [edit]

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:50 [edit]

for X being set

for Si being SigmaField of X

for A being Event of Si holds A ` is Event of Si by Def1;

for Si being SigmaField of X

for A being Event of Si holds A ` is Event of Si by Def1;

theorem :: PROB_1:51 [edit]

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 Th9;

for Si being SigmaField of X

for A, B being Event of Si holds A \/ B is Event of Si by Th9;

theorem :: PROB_1:52 [edit]

theorem :: PROB_1:53 [edit]

theorem :: PROB_1:54 [edit]

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 Th12;

for Si being SigmaField of X

for A, B being Event of Si holds A \ B is Event of Si by Th12;

registration

let X be set ;

let Si be SigmaField of X;

cluster empty Event of ;

existence

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

end;
let Si be SigmaField of X;

cluster empty Event of ;

existence

ex b

proof end;

definition

canceled;

let X be set ;

let Si be SigmaField of X;

canceled;

func [#] Si -> Event of Si equals :: PROB_1:def 11

X;

coherence

X is Event of Si by Th11;

end;
let X be set ;

let Si be SigmaField of X;

canceled;

func [#] Si -> Event of Si equals :: PROB_1:def 11

X;

coherence

X is Event of Si by Th11;

:: deftheorem PROB_1:def 9 :

canceled;

:: deftheorem PROB_1:def 10 :

canceled;

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

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 Th9;

:: original: \

redefine func A \ B -> Event of Si;

coherence

A \ B is Event of Si by Th12;

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 Th9;

:: original: \

redefine func A \ B -> Event of Si;

coherence

A \ B is Event of Si by Th12;

theorem :: PROB_1:55

canceled;

theorem :: PROB_1:56

canceled;

theorem :: PROB_1:57 [edit]

for Omega being non empty set

for ASeq being SetSequence of Omega

for Sigma being SigmaField of Omega holds

( ASeq is SetSequence of Sigma iff for n being Element of NAT holds ASeq . n is Event of Sigma )

for ASeq being SetSequence of Omega

for Sigma being SigmaField of Omega holds

( ASeq is SetSequence of Sigma iff for n being Element of NAT holds ASeq . n is Event of Sigma )

proof end;

theorem :: PROB_1:58 [edit]

for Omega being non empty 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 Th46;

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 Th46;

theorem Th59: :: PROB_1:59 [edit]

for Omega being non empty set

for 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 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 ) ) ) )

proof end;

theorem Th60: :: PROB_1:60 [edit]

for Omega being non empty set

for 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 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 ) )

proof end;

theorem :: PROB_1:61

canceled;

theorem Th62: :: PROB_1:62 [edit]

for Omega being non empty 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 non empty 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 Th62;

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 Th62;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

canceled;

mode Probability of Sigma -> Function of Sigma,REAL means :Def13: :: PROB_1:def 13

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

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;

canceled;

mode Probability of Sigma -> Function of Sigma,REAL means :Def13: :: PROB_1:def 13

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

ex b

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

b

( b

proof end;

:: deftheorem PROB_1:def 12 :

canceled;

:: deftheorem Def13 defines Probability PROB_1:def 13 :

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;

cluster -> zeroed Probability of Sigma;

coherence

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

end;
let Sigma be SigmaField of Omega;

cluster -> zeroed Probability of Sigma;

coherence

for b

proof end;

theorem :: PROB_1:63

canceled;

theorem :: PROB_1:64

canceled;

theorem :: PROB_1:65

canceled;

theorem :: PROB_1:66 [edit]

for Omega being non empty set

for Sigma being SigmaField of Omega

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

for Sigma being SigmaField of Omega

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

theorem Th67: :: PROB_1:67 [edit]

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:68 [edit]

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 Th69: :: PROB_1:69 [edit]

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 Th70: :: PROB_1:70 [edit]

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:71 [edit]

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 Th72: :: PROB_1:72 [edit]

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 Th73: :: PROB_1:73 [edit]

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 Th74: :: PROB_1:74 [edit]

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:75 [edit]

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;

theorem :: PROB_1:76 [edit]

Lm3: for Omega being non empty set

for X being Subset-Family of Omega ex Y being SigmaField of Omega st

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

Y c= Z ) )

proof end;

definition

let Omega be non empty set ;

let X be Subset-Family of Omega;

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

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

it c= Z ) );

existence

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 ) )
by Lm3;

uniqueness

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 14

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

it c= Z ) );

existence

ex b

( X c= b

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem defines sigma PROB_1:def 14 :

for Omega being non empty set

for X being Subset-Family of Omega

for b

( b

b

definition

let r be ext-real number ;

func halfline r -> Subset of REAL equals :: PROB_1:def 15

].-infty,r.[;

coherence

].-infty,r.[ is Subset of REAL

end;
func halfline r -> Subset of REAL equals :: PROB_1:def 15

].-infty,r.[;

coherence

].-infty,r.[ is Subset of REAL

proof end;

:: deftheorem defines halfline PROB_1:def 15 :

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

definition

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

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

coherence

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

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

coherence

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

proof end;

:: deftheorem defines Family_of_halflines PROB_1:def 16 :

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

definition

func Borel_Sets -> SigmaField of REAL equals :: PROB_1:def 17

sigma Family_of_halflines;

correctness

coherence

sigma Family_of_halflines is SigmaField of REAL;

;

end;
sigma Family_of_halflines;

correctness

coherence

sigma Family_of_halflines is SigmaField of REAL;

;

:: deftheorem defines Borel_Sets PROB_1:def 17 :

Borel_Sets = sigma Family_of_halflines;

theorem :: PROB_1:77 [edit]

for X being set

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

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