:: PROB_1 semantic presentation

Lm1: for r, r2 being real number st 0 <= r holds
r2 - r <= r2
by XREAL_1:45;

theorem :: PROB_1:1

canceled;

theorem :: PROB_1:2

canceled;

theorem Th3: :: PROB_1:3

for r being real number
for seq being Real_Sequence st ex n being Nat st
for m being 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;

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

registration

let X be set ;
cluster non empty cap-closed compl-closed Element of bool (bool X);
existence

proof end;

end;

definition

let X be set ;
mode Field_Subset of X is non empty cap-closed compl-closed Subset-Family of X;

end;

theorem Th4: :: PROB_1:4

for X being set
for A, B being Subset of X holds {A,B} is Subset-Family of X

proof end;

theorem :: PROB_1:5

canceled;

theorem Th6: :: PROB_1:6

for X being set
for F being Field_Subset of X ex A being Subset of X st A in F

proof end;

theorem :: PROB_1:7

canceled;

theorem :: PROB_1:8

canceled;

theorem Th9: :: PROB_1:9

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

proof end;

theorem Th10: :: PROB_1:10

for X being set
for F being Field_Subset of X holds {} in F

proof end;

theorem Th11: :: PROB_1:11

for X being set
for F being Field_Subset of X holds X in F

proof end;

theorem Th12: :: PROB_1:12

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

proof end;

theorem :: PROB_1:13

for X being set
for F being Field_Subset of X
for A, B being set holds
( A \ B misses B & ( A in F & B in F implies (A \ B) \/ B in F ) )

proof end;

theorem :: PROB_1:14

for X being set holds {{} ,X} is Field_Subset of X

proof end;

theorem :: PROB_1:15

for X being set holds bool X is Field_Subset of X

proof end;

theorem :: PROB_1:16

for X being set
for F being Field_Subset of X holds
( {{} ,X} c= F & F c= bool X )

proof end;

theorem :: PROB_1:17

canceled;

theorem :: PROB_1:18

for X being set holds
( ( for p being set st p in [:NAT ,{X}:] holds
ex x, y being set st [x,y] = p ) & ( for x, y, z being set st [x,y] in [:NAT ,{X}:] & [x,z] in [:NAT ,{X}:] holds
y = z ) )

proof end;

theorem Th19: :: PROB_1:19

for X being set ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = X ) )

proof end;

definition

let X be set ;
mode SetSequence of X is Function of NAT , bool X;

end;

Lm2: for X being set
for A1 being SetSequence of X holds
( dom A1 = NAT & ( for n being Nat holds A1 . n in bool X ) )
by FUNCT_2:def 1;

theorem :: PROB_1:20

canceled;

theorem Th21: :: PROB_1:21

for X being set ex A1 being SetSequence of X st
for n being Nat holds A1 . n = X

proof end;

theorem Th22: :: PROB_1:22

for X being set
for A, B being Subset of X ex A1 being SetSequence of X st
( A1 . 0 = A & ( for n being Nat st n <> 0 holds
A1 . n = B ) )

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
let n be Nat;
:: original: .
redefine func A1 . n -> Subset of X;
coherence by Lm2;

end;

theorem Th23: :: PROB_1:23

for X being set
for A1 being SetSequence of X holds union (rng A1) is Subset of X

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
:: original: Union
redefine func Union A1 -> Subset of X;
coherence

proof end;

end;

theorem :: PROB_1:24

canceled;

theorem Th25: :: PROB_1:25

for X, x being set
for A1 being SetSequence of X holds
( x in Union A1 iff ex n being Nat st x in A1 . n )

proof end;

theorem Th26: :: PROB_1:26

for X being set
for A1 being SetSequence of X ex B1 being SetSequence of X st
for n being 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 Nat holds it . n = (A1 . n) ` ;
existence by Th26;
uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem PROB_1:def 2 :

:: deftheorem PROB_1:def 3 :

:: deftheorem Def4 defines Complement PROB_1:def 4 :

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 ;

end;

:: deftheorem defines Intersection PROB_1:def 5 :

theorem :: PROB_1:27

canceled;

theorem :: PROB_1:28

canceled;

theorem Th29: :: PROB_1:29

for X, x being set
for A1 being SetSequence of X holds
( x in Intersection A1 iff for n being Nat holds x in A1 . n )

proof end;

theorem Th30: :: PROB_1:30

for X being set
for A1 being SetSequence of X
for A, B being Subset of X st A1 . 0 = A & ( for n being Nat st n <> 0 holds
A1 . n = B ) holds
Intersection A1 = A /\ B

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
attr A1 is non-increasing means :Def6: :: PROB_1:def 6
for n, m being Nat st n <= m holds
A1 . m c= A1 . n;
attr A1 is non-decreasing means :: PROB_1:def 7
for n, m being Nat st n <= m holds
A1 . n c= A1 . m;

end;

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

:: deftheorem defines non-decreasing PROB_1:def 7 :

definition

let X be set ;
mode SigmaField of X -> non empty Subset-Family of X means :Def8: :: PROB_1:def 8
( ( for A1 being SetSequence of X st ( for n being Nat holds A1 . n in it ) holds
Intersection A1 in it ) & ( for A being Subset of X st A in it holds
A ` in it ) );
existence

proof end;

end;

:: deftheorem Def8 defines SigmaField PROB_1:def 8 :

theorem :: PROB_1:31

canceled;

theorem Th32: :: PROB_1:32

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 ( for n being Nat holds A1 . n in S ) holds
Intersection A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) ) by Def8;

theorem :: PROB_1:33

canceled;

theorem :: PROB_1:34

canceled;

theorem Th35: :: PROB_1:35

for Y, X being set st Y is SigmaField of X holds
Y is Field_Subset of X

proof end;

registration

let X be set ;
cluster -> cap-closed compl-closed SigmaField of X;
coherence by Th35;

end;

theorem :: PROB_1:36

canceled;

theorem :: PROB_1:37

canceled;

theorem :: PROB_1:38

for X being set
for Si being SigmaField of X ex A being Subset of X st A in Si

proof end;

theorem :: PROB_1:39

canceled;

theorem :: PROB_1:40

canceled;

theorem :: PROB_1:41

for X being set
for Si being SigmaField of X
for A, B being Subset of X st A in Si & B in Si holds
A \/ B in Si by Th9;

theorem :: PROB_1:42

for X being set
for Si being SigmaField of X holds {} in Si by Th10;

theorem :: PROB_1:43

for X being set
for Si being SigmaField of X holds X in Si by Th11;

theorem :: PROB_1:44

for X being set
for Si being SigmaField of X
for A, B being Subset of X st A in Si & B in Si holds
A \ B in Si by Th12;

definition

let X be set ;
let Si be SigmaField of X;
mode SetSequence of Si -> SetSequence of X means :Def9: :: PROB_1:def 9
for n being Nat holds it . n in Si;
existence

proof end;

end;

:: deftheorem Def9 defines SetSequence PROB_1:def 9 :

theorem :: PROB_1:45

canceled;

theorem Th46: :: PROB_1:46

for X being set
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;
mode Event of F -> Subset of X means :Def10: :: PROB_1:def 10
it in F;
existence

proof end;

end;

:: deftheorem Def10 defines Event PROB_1:def 10 :

theorem :: PROB_1:47

canceled;

theorem :: PROB_1:48

for X, x being set
for Si being SigmaField of X st x in Si holds
x is Event of Si by Def10;

theorem Th49: :: PROB_1:49

for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A /\ B is Event of Si

proof end;

theorem :: PROB_1:50

for X being set
for Si being SigmaField of X
for A being Event of Si holds A ` is Event of Si

proof end;

theorem Th51: :: PROB_1:51

for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A \/ B is Event of Si

proof end;

theorem Th52: :: PROB_1:52

for X being set
for Si being SigmaField of X holds {} is Event of Si

proof end;

theorem Th53: :: PROB_1:53

for X being set
for Si being SigmaField of X holds X is Event of Si

proof end;

theorem Th54: :: PROB_1:54

for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A \ B is Event of Si

proof end;

registration

let X be set ;
let Si be SigmaField of X;
cluster empty Event of Si;
existence

proof end;

end;

definition

let X be set ;
let Si be SigmaField of X;
func [#] Si -> Event of Si equals :: PROB_1:def 11
X;
coherence by Th53;

end;

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

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 by Th49;
:: original: \/
redefine func A \/ B -> Event of Si;
coherence by Th51;
:: original: \
redefine func A \ B -> Event of Si;
coherence by Th54;

end;

theorem :: PROB_1:55

canceled;

theorem :: PROB_1:56

canceled;

theorem :: PROB_1:57

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 Nat holds ASeq . n is Event of Sigma )

proof end;

theorem :: PROB_1:58

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

proof end;

theorem Th59: :: PROB_1:59

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

proof end;

theorem Th60: :: PROB_1:60

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

proof end;

theorem :: PROB_1:61

canceled;

theorem Th62: :: PROB_1:62

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

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

end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Function of Sigma, REAL ;
let A be Event of Sigma;
:: original: .
redefine func P . A -> Real;
coherence

proof end;

end;

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-increasing holds
( it * ASeq is convergent & lim (it * ASeq) = it . (Intersection ASeq) ) ) );
existence

proof end;

end;

:: deftheorem PROB_1:def 12 :

:: deftheorem Def13 defines Probability PROB_1:def 13 :

theorem :: PROB_1:63

canceled;

theorem :: PROB_1:64

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P . {} = 0

proof end;

theorem :: PROB_1:65

canceled;

theorem :: PROB_1:66

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P . ([#] Sigma) = 1 by Def13;

theorem Th67: :: PROB_1:67

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

proof end;

theorem :: PROB_1:68

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)

proof end;

theorem Th69: :: PROB_1:69

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)

proof end;

theorem Th70: :: PROB_1:70

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

proof end;

theorem :: PROB_1:71

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

proof end;

theorem Th72: :: PROB_1:72

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

proof end;

theorem Th73: :: PROB_1:73

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

proof end;

theorem Th74: :: PROB_1:74

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

proof end;

theorem :: PROB_1:75

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)

proof end;

theorem Th76: :: PROB_1:76

for Omega being non empty set holds bool Omega is SigmaField of Omega

proof end;

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

proof end;

end;

:: deftheorem defines sigma PROB_1:def 14 :

definition

let r be real number ;
func halfline r -> Subset of REAL equals :: PROB_1:def 15
{ r1 where r1 is Element of REAL : r1 < r } ;
coherence

proof end;

end;

:: deftheorem defines halfline PROB_1:def 15 :

definition

func Family_of_halflines -> Subset-Family of REAL equals :: PROB_1:def 16
{ D where D is Subset of REAL : ex r being real number st D = halfline r } ;
coherence

proof end;

end;

:: deftheorem defines Family_of_halflines PROB_1:def 16 :

definition

func Borel_Sets -> SigmaField of REAL equals :: PROB_1:def 17
sigma Family_of_halflines ;
correctness ;

end;

:: deftheorem defines Borel_Sets PROB_1:def 17 :