:: PROB_3 semantic presentation

Lemma1: for b₁, b₂, b₃ being real number st 0 < b₃ & b₁ <= b₂ holds
( b₁ < b₂ + b₃ & b₁ - b₃ < b₂ )

proof end;

theorem Th1: :: PROB_3:1

for b₁ being FinSequence holds not 0 in dom b₁

proof end;

theorem Th2: :: PROB_3:2

for b₁ being Nat
for b₂ being FinSequence holds
( b₁ in dom b₂ iff ( b₁ <> 0 & b₁ <= len b₂ ) )

proof end;

theorem Th3: :: PROB_3: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;

theorem Th4: :: PROB_3:4

for b₁ being Nat
for b₂ being non empty set
for b₃ being SigmaField of b₂
for b₄ being SetSequence of b₃
for b₅ being Probability of b₃ holds (b₅ * b₄) . b₁ >= 0

proof end;

theorem Th5: :: PROB_3:5

for b₁ being Nat
for b₂ being non empty set
for b₃ being SigmaField of b₂
for b₄, b₅ being SetSequence of b₃
for b₆ being Probability of b₃ st b₄ . b₁ c= b₅ . b₁ holds
(b₆ * b₄) . b₁ <= (b₆ * b₅) . b₁

proof end;

theorem Th6: :: PROB_3:6

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ st b₃ is non-decreasing holds
b₄ * b₃ is non-decreasing

proof end;

theorem Th7: :: PROB_3:7

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ st b₃ is non-increasing holds
b₄ * b₃ is non-increasing

proof end;

theorem Th8: :: PROB_3:8

for b₁ being set
for b₂ being SetSequence of b₁ ex b₃ being SetSequence of b₁ st
( b₃ . 0 = b₂ . 0 & ( for b₄ being Nat holds b₃ . (b₄ + 1) = (b₃ . b₄) /\ (b₂ . (b₄ + 1)) ) )

proof end;

theorem Th9: :: PROB_3:9

for b₁ being set
for b₂ being SetSequence of b₁ ex b₃ being SetSequence of b₁ st
( b₃ . 0 = b₂ . 0 & ( for b₄ being Nat holds b₃ . (b₄ + 1) = (b₃ . b₄) \/ (b₂ . (b₄ + 1)) ) )

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func Partial_Intersection c₂ -> SetSequence of a₁ means :Def1: :: PROB_3:def 1
( a₃ . 0 = a₂ . 0 & ( for b₁ being Nat holds a₃ . (b₁ + 1) = (a₃ . b₁) /\ (a₂ . (b₁ + 1)) ) );
existence by Th8;
uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func Partial_Union c₂ -> SetSequence of a₁ means :Def2: :: PROB_3:def 2
( a₃ . 0 = a₂ . 0 & ( for b₁ being Nat holds a₃ . (b₁ + 1) = (a₃ . b₁) \/ (a₂ . (b₁ + 1)) ) );
existence by Th9;
uniqueness

proof end;

end;

:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :

theorem Th10: :: PROB_3:10

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (Partial_Intersection b₃) . b₁ c= b₃ . b₁

proof end;

theorem Th11: :: PROB_3:11

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds b₃ . b₁ c= (Partial_Union b₃) . b₁

proof end;

theorem Th12: :: PROB_3:12

for b₁ being set
for b₂ being SetSequence of b₁ holds Partial_Intersection b₂ is non-increasing

proof end;

theorem Th13: :: PROB_3:13

for b₁ being set
for b₂ being SetSequence of b₁ holds Partial_Union b₂ is non-decreasing

proof end;

theorem Th14: :: PROB_3:14

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SetSequence of b₂ holds
( b₃ in (Partial_Intersection b₄) . b₁ iff for b₅ being Nat st b₅ <= b₁ holds
b₃ in b₄ . b₅ )

proof end;

theorem Th15: :: PROB_3:15

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SetSequence of b₂ holds
( b₃ in (Partial_Union b₄) . b₁ iff ex b₅ being Nat st
( b₅ <= b₁ & b₃ in b₄ . b₅ ) )

proof end;

theorem Th16: :: PROB_3:16

for b₁ being set
for b₂ being SetSequence of b₁ holds Intersection (Partial_Intersection b₂) = Intersection b₂

proof end;

theorem Th17: :: PROB_3:17

for b₁ being set
for b₂ being SetSequence of b₁ holds Union (Partial_Union b₂) = Union b₂

proof end;

theorem Th18: :: PROB_3:18

for b₁ being set
for b₂ being SetSequence of b₁ ex b₃ being SetSequence of b₁ st
( b₃ . 0 = b₂ . 0 & ( for b₄ being Nat holds b₃ . (b₄ + 1) = (b₂ . (b₄ + 1)) \ ((Partial_Union b₂) . b₄) ) )

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func Partial_Diff_Union c₂ -> SetSequence of a₁ means :Def3: :: PROB_3:def 3
( a₃ . 0 = a₂ . 0 & ( for b₁ being Nat holds a₃ . (b₁ + 1) = (a₂ . (b₁ + 1)) \ ((Partial_Union a₂) . b₁) ) );
existence by Th18;
uniqueness

proof end;

end;

:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :

theorem Th19: :: PROB_3:19

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SetSequence of b₂ holds
( b₃ in (Partial_Diff_Union b₄) . b₁ iff ( b₃ in b₄ . b₁ & ( for b₅ being Nat st b₅ < b₁ holds
not b₃ in b₄ . b₅ ) ) )

proof end;

theorem Th20: :: PROB_3:20

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (Partial_Diff_Union b₃) . b₁ c= b₃ . b₁

proof end;

theorem Th21: :: PROB_3:21

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (Partial_Diff_Union b₃) . b₁ c= (Partial_Union b₃) . b₁

proof end;

theorem Th22: :: PROB_3:22

for b₁ being set
for b₂ being SetSequence of b₁ holds Partial_Union (Partial_Diff_Union b₂) = Partial_Union b₂

proof end;

theorem Th23: :: PROB_3:23

for b₁ being set
for b₂ being SetSequence of b₁ holds Union (Partial_Diff_Union b₂) = Union b₂

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
redefine attr disjoint_valued as a₂ is disjoint_valued means :Def4: :: PROB_3:def 4
for b₁, b₂ being Nat st b₁ <> b₂ holds
a₂ . b₁ misses a₂ . b₂;
compatibility

proof end;

end;

:: deftheorem Def4 defines disjoint_valued PROB_3:def 4 :

theorem Th24: :: PROB_3:24

for b₁ being set
for b₂ being SetSequence of b₁ holds Partial_Diff_Union b₂ is disjoint_valued

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func @Partial_Intersection c₃ -> SetSequence of a₂ equals :: PROB_3:def 5
Partial_Intersection a₃;
coherence

proof end;

end;

:: deftheorem Def5 defines @Partial_Intersection PROB_3:def 5 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func @Partial_Union c₃ -> SetSequence of a₂ equals :: PROB_3:def 6
Partial_Union a₃;
coherence

proof end;

end;

:: deftheorem Def6 defines @Partial_Union PROB_3:def 6 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func @Partial_Diff_Union c₃ -> SetSequence of a₂ equals :: PROB_3:def 7
Partial_Diff_Union a₃;
coherence

proof end;

end;

:: deftheorem Def7 defines @Partial_Diff_Union PROB_3:def 7 :

theorem Th25: :: PROB_3:25

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being SetSequence of b₂ st b₃ = @Partial_Intersection b₄ holds
( b₃ . 0 = b₄ . 0 & ( for b₅ being Nat holds b₃ . (b₅ + 1) = (b₃ . b₅) /\ (b₄ . (b₅ + 1)) ) ) by Def1;

theorem Th26: :: PROB_3:26

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being SetSequence of b₂ st b₃ = @Partial_Union b₄ holds
( b₃ . 0 = b₄ . 0 & ( for b₅ being Nat holds b₃ . (b₅ + 1) = (b₃ . b₅) \/ (b₄ . (b₅ + 1)) ) ) by Def2;

theorem Th27: :: PROB_3:27

for b₁ being Nat
for b₂ being set
for b₃ being SigmaField of b₂
for b₄ being SetSequence of b₃ holds (@Partial_Intersection b₄) . b₁ c= b₄ . b₁ by Th10;

theorem Th28: :: PROB_3:28

for b₁ being Nat
for b₂ being set
for b₃ being SigmaField of b₂
for b₄ being SetSequence of b₃ holds b₄ . b₁ c= (@Partial_Union b₄) . b₁ by Th11;

theorem Th29: :: PROB_3:29

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SigmaField of b₂
for b₅ being SetSequence of b₄ holds
( b₃ in (@Partial_Intersection b₅) . b₁ iff for b₆ being Nat st b₆ <= b₁ holds
b₃ in b₅ . b₆ ) by Th14;

theorem Th30: :: PROB_3:30

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SigmaField of b₂
for b₅ being SetSequence of b₄ holds
( b₃ in (@Partial_Union b₅) . b₁ iff ex b₆ being Nat st
( b₆ <= b₁ & b₃ in b₅ . b₆ ) ) by Th15;

theorem Th31: :: PROB_3:31

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds @Partial_Intersection b₃ is non-increasing by Th12;

theorem Th32: :: PROB_3:32

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds @Partial_Union b₃ is non-decreasing by Th13;

theorem Th33: :: PROB_3:33

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds Intersection (@Partial_Intersection b₃) = Intersection b₃ by Th16;

theorem Th34: :: PROB_3:34

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds Union (@Partial_Union b₃) = Union b₃ by Th17;

theorem Th35: :: PROB_3:35

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄ being SetSequence of b₂ st b₃ = @Partial_Diff_Union b₄ holds
( b₃ . 0 = b₄ . 0 & ( for b₅ being Nat holds b₃ . (b₅ + 1) = (b₄ . (b₅ + 1)) \ ((@Partial_Union b₄) . b₅) ) ) by Def3;

theorem Th36: :: PROB_3:36

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SigmaField of b₂
for b₅ being SetSequence of b₄ holds
( b₃ in (@Partial_Diff_Union b₅) . b₁ iff ( b₃ in b₅ . b₁ & ( for b₆ being Nat st b₆ < b₁ holds
not b₃ in b₅ . b₆ ) ) ) by Th19;

theorem Th37: :: PROB_3:37

for b₁ being Nat
for b₂ being set
for b₃ being SigmaField of b₂
for b₄ being SetSequence of b₃ holds (@Partial_Diff_Union b₄) . b₁ c= b₄ . b₁ by Th20;

theorem Th38: :: PROB_3:38

for b₁ being Nat
for b₂ being set
for b₃ being SigmaField of b₂
for b₄ being SetSequence of b₃ holds (@Partial_Diff_Union b₄) . b₁ c= (@Partial_Union b₄) . b₁ by Th21;

theorem Th39: :: PROB_3:39

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds @Partial_Union (@Partial_Diff_Union b₃) = @Partial_Union b₃ by Th22;

theorem Th40: :: PROB_3:40

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds Union (@Partial_Diff_Union b₃) = Union b₃ by Th23;

theorem Th41: :: PROB_3:41

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds @Partial_Diff_Union b₃ is disjoint_valued by Th24;

theorem Th42: :: PROB_3:42

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds b₄ * (@Partial_Union b₃) is non-decreasing

proof end;

theorem Th43: :: PROB_3:43

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds b₄ * (@Partial_Intersection b₃) is non-increasing

proof end;

theorem Th44: :: PROB_3:44

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds Partial_Sums (b₄ * b₃) is non-decreasing

proof end;

theorem Th45: :: PROB_3:45

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds (b₄ * (@Partial_Union b₃)) . 0 = (Partial_Sums (b₄ * b₃)) . 0

proof end;

theorem Th46: :: PROB_3:46

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ holds
( b₄ * (@Partial_Union b₃) is convergent & lim (b₄ * (@Partial_Union b₃)) = sup (b₄ * (@Partial_Union b₃)) & lim (b₄ * (@Partial_Union b₃)) = b₄ . (Union b₃) )

proof end;

theorem Th47: :: PROB_3:47

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is disjoint_valued holds
for b₄, b₅ being Nat st b₄ < b₅ holds
(@Partial_Union b₃) . b₄ misses b₃ . b₅

proof end;

theorem Th48: :: PROB_3:48

for b₁ being Nat
for b₂ being non empty set
for b₃ being SigmaField of b₂
for b₄ being SetSequence of b₃
for b₅ being Probability of b₃ st b₄ is disjoint_valued holds
(b₅ * (@Partial_Union b₄)) . b₁ = (Partial_Sums (b₅ * b₄)) . b₁

proof end;

theorem Th49: :: PROB_3:49

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ st b₃ is disjoint_valued holds
b₄ * (@Partial_Union b₃) = Partial_Sums (b₄ * b₃)

proof end;

theorem Th50: :: PROB_3:50

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ st b₃ is disjoint_valued holds
( Partial_Sums (b₄ * b₃) is convergent & lim (Partial_Sums (b₄ * b₃)) = sup (Partial_Sums (b₄ * b₃)) & lim (Partial_Sums (b₄ * b₃)) = b₄ . (Union b₃) )

proof end;

theorem Th51: :: PROB_3:51

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂
for b₄ being Probability of b₂ st b₃ is disjoint_valued holds
b₄ . (Union b₃) = Sum (b₄ * b₃)

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> Subset of a₁;
coherence

proof end;

end;

theorem Th52: :: PROB_3:52

for b₁ being set ex b₂ being FinSequence of bool b₁ st
for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = b₁

proof end;

theorem Th53: :: PROB_3:53

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

proof end;

definition

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

proof end;

end;

theorem Th54: :: PROB_3:54

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

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
func Complement c₂ -> FinSequence of bool a₁ means :Def8: :: PROB_3:def 8
( len a₃ = len a₂ & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ = (a₂ . b₁) ` ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Complement PROB_3:def 8 :

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
func Intersection c₂ -> Subset of a₁ equals :Def9: :: PROB_3:def 9
(Union (Complement a₂)) ` if a₂ <> {}
otherwise {} ;
coherence by SUBSET_1:4;
consistency ;

end;

:: deftheorem Def9 defines Intersection PROB_3:def 9 :

theorem Th55: :: PROB_3:55

for b₁ being set
for b₂ being FinSequence of bool b₁ holds dom (Complement b₂) = dom b₂

proof end;

theorem Th56: :: PROB_3:56

for b₁, b₂ being set
for b₃ being FinSequence of bool b₁ st b₃ <> {} holds
( b₂ in Intersection b₃ iff for b₄ being Nat st b₄ in dom b₃ holds
b₂ in b₃ . b₄ )

proof end;

theorem Th57: :: PROB_3:57

for b₁, b₂ being set
for b₃ being FinSequence of bool b₁ st b₃ <> {} holds
( b₂ in meet (rng b₃) iff for b₄ being Nat st b₄ in dom b₃ holds
b₂ in b₃ . b₄ )

proof end;

theorem Th58: :: PROB_3:58

for b₁ being set
for b₂ being FinSequence of bool b₁ holds Intersection b₂ = meet (rng b₂)

proof end;

theorem Th59: :: PROB_3:59

for b₁ being set
for b₂ being FinSequence of bool b₁ ex b₃ being SetSequence of b₁ st
( ( for b₄ being Nat st b₄ in dom b₂ holds
b₃ . b₄ = b₂ . b₄ ) & ( for b₄ being Nat st not b₄ in dom b₂ holds
b₃ . b₄ = {} ) )

proof end;

theorem Th60: :: PROB_3:60

for b₁ being set
for b₂ being FinSequence of bool b₁
for b₃ being SetSequence of b₁ st ( for b₄ being Nat st b₄ in dom b₂ holds
b₃ . b₄ = b₂ . b₄ ) & ( for b₄ being Nat st not b₄ in dom b₂ holds
b₃ . b₄ = {} ) holds
( b₃ . 0 = {} & Union b₃ = Union b₂ )

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
mode FinSequence of c₂ -> FinSequence of bool a₁ means :Def10: :: PROB_3:def 10
for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ in a₂;
existence

proof end;

end;

:: deftheorem Def10 defines FinSequence PROB_3:def 10 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be FinSequence of c₂;
let c₄ be Nat;
redefine func . as c₃ . c₄ -> Event of a₂;
coherence

proof end;

end;

theorem Th61: :: PROB_3:61

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being FinSequence of b₂ ex b₄ being SetSequence of b₂ st
( ( for b₅ being Nat st b₅ in dom b₃ holds
b₄ . b₅ = b₃ . b₅ ) & ( for b₅ being Nat st not b₅ in dom b₃ holds
b₄ . b₅ = {} ) )

proof end;

theorem Th62: :: PROB_3:62

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

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be FinSequence of c₂;
func @Complement c₃ -> FinSequence of a₂ equals :: PROB_3:def 11
Complement a₃;
coherence

proof end;

end;

:: deftheorem Def11 defines @Complement PROB_3:def 11 :

theorem Th63: :: PROB_3:63

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being FinSequence of b₂ holds Intersection b₃ in b₂

proof end;

theorem Th64: :: PROB_3:64

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being FinSequence of b₂ holds dom (b₃ * b₄) = dom b₄

proof end;

theorem Th65: :: PROB_3:65

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being FinSequence of b₂ holds b₃ * b₄ is FinSequence of REAL

proof end;

definition

let c₁ be non empty set ;
let c₂ be SigmaField of c₁;
let c₃ be FinSequence of c₂;
let c₄ be Probability of c₂;
redefine func * as c₄ * c₃ -> FinSequence of REAL ;
coherence by Th65;

end;

theorem Th66: :: PROB_3:66

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being FinSequence of b₂ holds len (b₃ * b₄) = len b₄

proof end;

theorem Th67: :: PROB_3:67

for b₁ being FinSequence of REAL st len b₁ = 0 holds
Sum b₁ = 0

proof end;

theorem Th68: :: PROB_3:68

for b₁ being FinSequence of REAL st len b₁ >= 1 holds
ex b₂ being Real_Sequence st
( b₂ . 1 = b₁ . 1 & ( for b₃ being Nat st 0 <> b₃ & b₃ < len b₁ holds
b₂ . (b₃ + 1) = (b₂ . b₃) + (b₁ . (b₃ + 1)) ) & Sum b₁ = b₂ . (len b₁) )

proof end;

theorem Th69: :: PROB_3:69

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being FinSequence of b₂
for b₅ being SetSequence of b₂ st ( for b₆ being Nat st b₆ in dom b₄ holds
b₅ . b₆ = b₄ . b₆ ) & ( for b₆ being Nat st not b₆ in dom b₄ holds
b₅ . b₆ = {} ) holds
( Partial_Sums (b₃ * b₅) is convergent & Sum (b₃ * b₅) = (Partial_Sums (b₃ * b₅)) . (len b₄) & b₃ . (Union b₅) <= Sum (b₃ * b₅) & Sum (b₃ * b₄) = Sum (b₃ * b₅) )

proof end;

theorem Th70: :: PROB_3:70

for b₁ being non empty set
for b₂ being SigmaField of b₁
for b₃ being Probability of b₂
for b₄ being FinSequence of b₂ holds
( b₃ . (Union b₄) <= Sum (b₃ * b₄) & ( b₄ is disjoint_valued implies b₃ . (Union b₄) = Sum (b₃ * b₄) ) )

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
attr a₂ is non-decreasing-closed means :Def12: :: PROB_3:def 12
for b₁ being SetSequence of a₁ st b₁ is non-decreasing & ( for b₂ being Nat holds b₁ . b₂ in a₂ ) holds
Union b₁ in a₂;
attr a₂ is non-increasing-closed means :Def13: :: PROB_3:def 13
for b₁ being SetSequence of a₁ st b₁ is non-increasing & ( for b₂ being Nat holds b₁ . b₂ in a₂ ) holds
Intersection b₁ in a₂;

end;

:: deftheorem Def12 defines non-decreasing-closed PROB_3:def 12 :

:: deftheorem Def13 defines non-increasing-closed PROB_3:def 13 :

theorem Th71: :: PROB_3:71

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ is non-decreasing-closed iff for b₃ being SetSequence of b₁ st b₃ is non-decreasing & ( for b₄ being Nat holds b₃ . b₄ in b₂ ) holds
lim b₃ in b₂ )

proof end;

theorem Th72: :: PROB_3:72

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ is non-increasing-closed iff for b₃ being SetSequence of b₁ st b₃ is non-increasing & ( for b₄ being Nat holds b₃ . b₄ in b₂ ) holds
lim b₃ in b₂ )

proof end;

theorem Th73: :: PROB_3:73

for b₁ being set holds
( bool b₁ is non-decreasing-closed & bool b₁ is non-increasing-closed )

proof end;

definition

let c₁ be set ;
mode MonotoneClass of c₁ -> Subset-Family of a₁ means :Def14: :: PROB_3:def 14
( a₂ is non-decreasing-closed & a₂ is non-increasing-closed );
existence

proof end;

end;

:: deftheorem Def14 defines MonotoneClass PROB_3:def 14 :

theorem Th74: :: PROB_3:74

for b₁, b₂ being set holds
( b₁ is MonotoneClass of b₂ iff ( b₁ c= bool b₂ & ( for b₃ being SetSequence of b₂ st b₃ is monotone & ( for b₄ being Nat holds b₃ . b₄ in b₁ ) holds
lim b₃ in b₁ ) ) )

proof end;

theorem Th75: :: PROB_3:75

for b₁ being set
for b₂ being Field_Subset of b₁ holds
( b₂ is SigmaField of b₁ iff b₂ is MonotoneClass of b₁ )

proof end;

theorem Th76: :: PROB_3:76

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

proof end;

theorem Th77: :: PROB_3:77

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
func monotoneclass c₂ -> MonotoneClass of a₁ means :Def15: :: PROB_3:def 15
( a₂ c= a₃ & ( for b₁ being set st a₂ c= b₁ & b₁ is MonotoneClass of a₁ holds
a₃ c= b₁ ) );
existence by Th77;
uniqueness

proof end;

end;

:: deftheorem Def15 defines monotoneclass PROB_3:def 15 :

theorem Th78: :: PROB_3:78

for b₁ being non empty set
for b₂ being Field_Subset of b₁ holds monotoneclass b₂ is Field_Subset of b₁

proof end;

theorem Th79: :: PROB_3:79

for b₁ being non empty set
for b₂ being Field_Subset of b₁ holds sigma b₂ = monotoneclass b₂

proof end;