:: PROB_1 semantic presentation

Lemma1: for b₁, b₂ being real number st 0 <= b₁ holds
b₂ - b₁ <= b₂
by XREAL_1:45;

theorem Th1: :: PROB_1:1

canceled;

theorem Th2: :: PROB_1:2

canceled;

theorem Th3: :: PROB_1:3

for b₁ being real number
for b₂ being Real_Sequence st ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ = b₁ holds
( b₂ is convergent & lim b₂ = b₁ )

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
attr a₂ is compl-closed means :Def1: :: PROB_1:def 1
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ ` in a₂;

end;

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

registration

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

proof end;

end;

definition

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

end;

theorem Th4: :: PROB_1:4

for b₁ being set
for b₂, b₃ being Subset of b₁ holds {b₂,b₃} is Subset-Family of b₁

proof end;

theorem Th5: :: PROB_1:5

canceled;

theorem Th6: :: PROB_1:6

for b₁ being set
for b₂ being Field_Subset of b₁ ex b₃ being Subset of b₁ st b₃ in b₂

proof end;

theorem Th7: :: PROB_1:7

canceled;

theorem Th8: :: PROB_1:8

canceled;

theorem Th9: :: PROB_1:9

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃, b₄ being set st b₃ in b₂ & b₄ in b₂ holds
b₃ \/ b₄ in b₂

proof end;

theorem Th10: :: PROB_1:10

for b₁ being set
for b₂ being Field_Subset of b₁ holds {} in b₂

proof end;

theorem Th11: :: PROB_1:11

for b₁ being set
for b₂ being Field_Subset of b₁ holds b₁ in b₂

proof end;

theorem Th12: :: PROB_1:12

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ \ b₄ in b₂

proof end;

theorem Th13: :: PROB_1:13

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃, b₄ being set holds
( b₃ \ b₄ misses b₄ & ( b₃ in b₂ & b₄ in b₂ implies (b₃ \ b₄) \/ b₄ in b₂ ) )

proof end;

theorem Th14: :: PROB_1:14

for b₁ being set holds {{} ,b₁} is Field_Subset of b₁

proof end;

theorem Th15: :: PROB_1:15

for b₁ being set holds bool b₁ is Field_Subset of b₁

proof end;

theorem Th16: :: PROB_1:16

for b₁ being set
for b₂ being Field_Subset of b₁ holds
( {{} ,b₁} c= b₂ & b₂ c= bool b₁ )

proof end;

theorem Th17: :: PROB_1:17

canceled;

theorem Th18: :: PROB_1:18

for b₁ being set holds
( ( for b₂ being set st b₂ in [:NAT ,{b₁}:] holds
ex b₃, b₄ being set st [b₃,b₄] = b₂ ) & ( for b₂, b₃, b₄ being set st [b₂,b₃] in [:NAT ,{b₁}:] & [b₂,b₄] in [:NAT ,{b₁}:] holds
b₃ = b₄ ) )

proof end;

theorem Th19: :: PROB_1:19

for b₁ being set ex b₂ being Function st
( dom b₂ = NAT & ( for b₃ being Nat holds b₂ . b₃ = b₁ ) )

proof end;

definition

let c₁ be set ;
mode SetSequence of a₁ is Function of NAT , bool a₁;

end;

Lemma11: for b₁ being set
for b₂ being SetSequence of b₁ holds
( dom b₂ = NAT & ( for b₃ being Nat holds b₂ . b₃ in bool b₁ ) )
by FUNCT_2:def 1;

theorem Th20: :: PROB_1:20

canceled;

theorem Th21: :: PROB_1:21

for b₁ being set ex b₂ being SetSequence of b₁ st
for b₃ being Nat holds b₂ . b₃ = b₁

proof end;

theorem Th22: :: PROB_1:22

for b₁ being set
for b₂, b₃ being Subset of b₁ ex b₄ being SetSequence of b₁ st
( b₄ . 0 = b₂ & ( for b₅ being Nat st b₅ <> 0 holds
b₄ . b₅ = b₃ ) )

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> Subset of a₁;
coherence by Lemma11;

end;

theorem Th23: :: PROB_1:23

for b₁ being set
for b₂ being SetSequence of b₁ holds union (rng b₂) is Subset of b₁

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
redefine func Union as Union c₂ -> Subset of a₁;
coherence

proof end;

end;

theorem Th24: :: PROB_1:24

canceled;

theorem Th25: :: PROB_1:25

for b₁, b₂ being set
for b₃ being SetSequence of b₁ holds
( b₂ in Union b₃ iff ex b₄ being Nat st b₂ in b₃ . b₄ )

proof end;

theorem Th26: :: PROB_1:26

for b₁ being set
for b₂ being SetSequence of b₁ ex b₃ being SetSequence of b₁ st
for b₄ being Nat holds b₃ . b₄ = (b₂ . b₄) `

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
canceled;
canceled;
func Complement c₂ -> SetSequence of a₁ means :Def4: :: PROB_1:def 4
for b₁ being Nat holds a₃ . b₁ = (a₂ . b₁) ` ;
existence by Th26;
uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def2 PROB_1:def 2 :

:: deftheorem Def3 PROB_1:def 3 :

:: deftheorem Def4 defines Complement PROB_1:def 4 :

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func Intersection c₂ -> Subset of a₁ equals :: PROB_1:def 5
(Union (Complement a₂)) ` ;
correctness ;

end;

:: deftheorem Def5 defines Intersection PROB_1:def 5 :

theorem Th27: :: PROB_1:27

canceled;

theorem Th28: :: PROB_1:28

canceled;

theorem Th29: :: PROB_1:29

for b₁, b₂ being set
for b₃ being SetSequence of b₁ holds
( b₂ in Intersection b₃ iff for b₄ being Nat holds b₂ in b₃ . b₄ )

proof end;

theorem Th30: :: PROB_1:30

for b₁ being set
for b₂ being SetSequence of b₁
for b₃, b₄ being Subset of b₁ st b₂ . 0 = b₃ & ( for b₅ being Nat st b₅ <> 0 holds
b₂ . b₅ = b₄ ) holds
Intersection b₂ = b₃ /\ b₄

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
attr a₂ is non-increasing means :Def6: :: PROB_1:def 6
for b₁, b₂ being Nat st b₁ <= b₂ holds
a₂ . b₂ c= a₂ . b₁;
attr a₂ is non-decreasing means :: PROB_1:def 7
for b₁, b₂ being Nat st b₁ <= b₂ holds
a₂ . b₁ c= a₂ . b₂;

end;

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

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

definition

let c₁ be set ;
mode SigmaField of c₁ -> non empty Subset-Family of a₁ means :Def8: :: PROB_1:def 8
( ( for b₁ being SetSequence of a₁ st ( for b₂ being Nat holds b₁ . b₂ in a₂ ) holds
Intersection b₁ in a₂ ) & ( for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ ` in a₂ ) );
existence

proof end;

end;

:: deftheorem Def8 defines SigmaField PROB_1:def 8 :

theorem Th31: :: PROB_1:31

canceled;

theorem Th32: :: PROB_1:32

for b₁ being set
for b₂ being non empty set holds
( b₂ is SigmaField of b₁ iff ( b₂ c= bool b₁ & ( for b₃ being SetSequence of b₁ st ( for b₄ being Nat holds b₃ . b₄ in b₂ ) holds
Intersection b₃ in b₂ ) & ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ ` in b₂ ) ) ) by Def8;

theorem Th33: :: PROB_1:33

canceled;

theorem Th34: :: PROB_1:34

canceled;

theorem Th35: :: PROB_1:35

for b₁, b₂ being set st b₁ is SigmaField of b₂ holds
b₁ is Field_Subset of b₂

proof end;

registration

let c₁ be set ;
cluster -> cap-closed compl-closed SigmaField of a₁;
coherence by Th35;

end;

theorem Th36: :: PROB_1:36

canceled;

theorem Th37: :: PROB_1:37

canceled;

theorem Th38: :: PROB_1:38

for b₁ being set
for b₂ being SigmaField of b₁ ex b₃ being Subset of b₁ st b₃ in b₂

proof end;

theorem Th39: :: PROB_1:39

canceled;

theorem Th40: :: PROB_1:40

canceled;

theorem Th41: :: PROB_1:41

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ \/ b₄ in b₂ by Th9;

theorem Th42: :: PROB_1:42

for b₁ being set
for b₂ being SigmaField of b₁ holds {} in b₂ by Th10;

theorem Th43: :: PROB_1:43

for b₁ being set
for b₂ being SigmaField of b₁ holds b₁ in b₂ by Th11;

theorem Th44: :: PROB_1:44

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ \ b₄ in b₂ by Th12;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
mode SetSequence of c₂ -> SetSequence of a₁ means :Def9: :: PROB_1:def 9
for b₁ being Nat holds a₃ . b₁ in a₂;
existence

proof end;

end;

:: deftheorem Def9 defines SetSequence PROB_1:def 9 :

theorem Th45: :: PROB_1:45

canceled;

theorem Th46: :: PROB_1:46

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds Union b₃ in b₂

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
mode Event of c₂ -> Subset of a₁ means :Def10: :: PROB_1:def 10
a₃ in a₂;
existence

proof end;

end;

:: deftheorem Def10 defines Event PROB_1:def 10 :

theorem Th47: :: PROB_1:47

canceled;

theorem Th48: :: PROB_1:48

for b₁, b₂ being set
for b₃ being SigmaField of b₁ st b₂ in b₃ holds
b₂ is Event of b₃ by Def10;

theorem Th49: :: PROB_1:49

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂ holds b₃ /\ b₄ is Event of b₂

proof end;

theorem Th50: :: PROB_1:50

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being Event of b₂ holds b₃ ` is Event of b₂

proof end;

theorem Th51: :: PROB_1:51

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂ holds b₃ \/ b₄ is Event of b₂

proof end;

theorem Th52: :: PROB_1:52

for b₁ being set
for b₂ being SigmaField of b₁ holds {} is Event of b₂

proof end;

theorem Th53: :: PROB_1:53

for b₁ being set
for b₂ being SigmaField of b₁ holds b₁ is Event of b₂

proof end;

theorem Th54: :: PROB_1:54

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂ holds b₃ \ b₄ is Event of b₂

proof end;

registration

let c₁ be set ;
let c₂ be SigmaField of c₁;
cluster empty Event of a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
func [#] c₂ -> Event of a₂ equals :: PROB_1:def 11
a₁;
coherence by Th53;

end;

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

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃, c₄ be Event of c₂;
redefine func /\ as c₃ /\ c₄ -> Event of a₂;
coherence by Th49;
redefine func \/ as c₃ \/ c₄ -> Event of a₂;
coherence by Th51;
redefine func \ as c₃ \ c₄ -> Event of a₂;
coherence by Th54;

end;

theorem Th55: :: PROB_1:55

canceled;

theorem Th56: :: PROB_1:56

canceled;

theorem Th57: :: PROB_1:57

for b₁ being non empty set
for b₂ being SetSequence of b₁
for b₃ being SigmaField of b₁ holds
( b₂ is SetSequence of b₃ iff for b₄ being Nat holds b₂ . b₄ is Event of b₃ )

proof end;

theorem Th58: :: PROB_1:58

for b₁ being non empty set
for b₂ being SetSequence of b₁
for b₃ being SigmaField of b₁ st b₂ is SetSequence of b₃ holds
Union b₂ is Event of b₃

proof end;

theorem Th59: :: PROB_1:59

for b₁ being non empty set
for b₂ being set
for b₃ being SigmaField of b₁ ex b₄ being Function st
( dom b₄ = b₃ & ( for b₅ being Subset of b₁ st b₅ in b₃ holds
( ( b₂ in b₅ implies b₄ . b₅ = 1 ) & ( not b₂ in b₅ implies b₄ . b₅ = 0 ) ) ) )

proof end;

theorem Th60: :: PROB_1:60

for b₁ being non empty set
for b₂ being set
for b₃ being SigmaField of b₁ ex b₄ being Function of b₃, REAL st
for b₅ being Subset of b₁ st b₅ in b₃ holds
( ( b₂ in b₅ implies b₄ . b₅ = 1 ) & ( not b₂ in b₅ implies b₄ . b₅ = 0 ) )

proof end;

theorem Th61: :: PROB_1:61

canceled;

theorem Th62: :: PROB_1:62

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Function of b₂, REAL holds b₄ * b₃ is Real_Sequence

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
let c₄ be Function of c₂, REAL ;
redefine func * as c₄ * c₃ -> Real_Sequence;
coherence by Th62;

end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be Function of c₂, REAL ;
let c₄ be Event of c₂;
redefine func . as c₃ . c₄ -> Real;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
canceled;
mode Probability of c₂ -> Function of a₂, REAL means :Def13: :: PROB_1:def 13
( ( for b₁ being Event of a₂ holds 0 <= a₃ . b₁ ) & a₃ . a₁ = 1 & ( for b₁, b₂ being Event of a₂ st b₁ misses b₂ holds
a₃ . (b₁ \/ b₂) = (a₃ . b₁) + (a₃ . b₂) ) & ( for b₁ being SetSequence of a₂ st b₁ is non-increasing holds
( a₃ * b₁ is convergent & lim (a₃ * b₁) = a₃ . (Intersection b₁) ) ) );
existence

proof end;

end;

:: deftheorem Def12 PROB_1:def 12 :

:: deftheorem Def13 defines Probability PROB_1:def 13 :

theorem Th63: :: PROB_1:63

canceled;

theorem Th64: :: PROB_1:64

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds b₃ . {} = 0

proof end;

theorem Th65: :: PROB_1:65

canceled;

theorem Th66: :: PROB_1:66

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂ holds b₃ . ([#] b₂) = 1 by Def13;

theorem Th67: :: PROB_1:67

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Event of b₂
for b₄ being Probability of b₂ holds (b₄ . (([#] b₂) \ b₃)) + (b₄ . b₃) = 1

proof end;

theorem Th68: :: PROB_1:68

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Event of b₂
for b₄ being Probability of b₂ holds b₄ . (([#] b₂) \ b₃) = 1 - (b₄ . b₃)

proof end;

theorem Th69: :: PROB_1:69

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂
for b₅ being Probability of b₂ st b₃ c= b₄ holds
b₅ . (b₄ \ b₃) = (b₅ . b₄) - (b₅ . b₃)

proof end;

theorem Th70: :: PROB_1:70

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂
for b₅ being Probability of b₂ st b₃ c= b₄ holds
b₅ . b₃ <= b₅ . b₄

proof end;

theorem Th71: :: PROB_1:71

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Event of b₂
for b₄ being Probability of b₂ holds b₄ . b₃ <= 1

proof end;

theorem Th72: :: PROB_1:72

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂
for b₅ being Probability of b₂ holds b₅ . (b₃ \/ b₄) = (b₅ . b₃) + (b₅ . (b₄ \ b₃))

proof end;

theorem Th73: :: PROB_1:73

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂
for b₅ being Probability of b₂ holds b₅ . (b₃ \/ b₄) = (b₅ . b₃) + (b₅ . (b₄ \ (b₃ /\ b₄)))

proof end;

theorem Th74: :: PROB_1:74

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂
for b₅ being Probability of b₂ holds b₅ . (b₃ \/ b₄) = ((b₅ . b₃) + (b₅ . b₄)) - (b₅ . (b₃ /\ b₄))

proof end;

theorem Th75: :: PROB_1:75

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃, b₄ being Event of b₂
for b₅ being Probability of b₂ holds b₅ . (b₃ \/ b₄) <= (b₅ . b₃) + (b₅ . b₄)

proof end;

theorem Th76: :: PROB_1:76

for b₁ being non empty set holds bool b₁ is SigmaField of b₁

proof end;

Lemma43: for b₁ being non empty set
for b₂ being Subset-Family of b₁ ex b₃ being SigmaField of b₁ st
( b₂ c= b₃ & ( for b₄ being set st b₂ c= b₄ & b₄ is SigmaField of b₁ holds
b₃ c= b₄ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
func sigma c₂ -> SigmaField of a₁ means :: PROB_1:def 14
( a₂ c= a₃ & ( for b₁ being set st a₂ c= b₁ & b₁ is SigmaField of a₁ holds
a₃ c= b₁ ) );
existence by Lemma43;
uniqueness

proof end;

end;

:: deftheorem Def14 defines sigma PROB_1:def 14 :

definition

let c₁ be real number ;
func halfline c₁ -> Subset of REAL equals :: PROB_1:def 15
{ b₁ where B is Element of REAL : b₁ < a₁ } ;
coherence

proof end;

end;

:: deftheorem Def15 defines halfline PROB_1:def 15 :

definition

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

proof end;

end;

:: deftheorem Def16 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 Def17 defines Borel_Sets PROB_1:def 17 :