:: Set Sequences and Monotone Class
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

Lm1: for t, p, s being Real st 0 < s & t <= p holds
( t < p + s & t - s < p )

proof end;

theorem Th1: :: PROB_3:1

for f being FinSequence holds not 0 in dom f

proof end;

theorem Th2: :: PROB_3:2

for n being Nat
for f being FinSequence holds
( n in dom f iff ( n <> 0 & n <= len f ) )

proof end;

theorem Th3: :: PROB_3:3

for g being Real
for f being Real_Sequence st ex k being Nat st
for n being Nat st k <= n holds
f . n = g holds
( f is convergent & lim f = g )

proof end;

theorem Th4: :: PROB_3:4

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * ASeq) . n >= 0

proof end;

theorem Th5: :: PROB_3:5

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq, BSeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq . n c= BSeq . n holds
(P * ASeq) . n <= (P * BSeq) . n

proof end;

theorem Th6: :: PROB_3:6

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V75() holds
P * ASeq is non-decreasing

proof end;

theorem Th7: :: PROB_3:7

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V74() holds
P * ASeq is non-increasing

proof end;

definition

let X be set ;
let A1 be SetSequence of X;

func Partial_Intersection A1 -> SetSequence of X means :Def1: :: PROB_3:def 1
( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) /\ (A1 . (n + 1)) ) );

existence
ex b₁ being SetSequence of X st
( b₁ . 0 = A1 . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) /\ (A1 . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of X st b₁ . 0 = A1 . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) /\ (A1 . (n + 1)) ) & b₂ . 0 = A1 . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) /\ (A1 . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Partial_Intersection A1 iff ( b₃ . 0 = A1 . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) /\ (A1 . (n + 1)) ) ) );

definition

let X be set ;
let A1 be SetSequence of X;

func Partial_Union A1 -> SetSequence of X means :Def2: :: PROB_3:def 2
( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ (A1 . (n + 1)) ) );

existence
ex b₁ being SetSequence of X st
( b₁ . 0 = A1 . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ (A1 . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of X st b₁ . 0 = A1 . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ (A1 . (n + 1)) ) & b₂ . 0 = A1 . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) \/ (A1 . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Partial_Union A1 iff ( b₃ . 0 = A1 . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) \/ (A1 . (n + 1)) ) ) );

theorem Th8: :: PROB_3:8

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n

proof end;

theorem Th9: :: PROB_3:9

for n being Nat
for X being set
for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

proof end;

theorem Th10: :: PROB_3:10

for X being set
for A1 being SetSequence of X holds Partial_Intersection A1 is V74()

proof end;

theorem Th11: :: PROB_3:11

for X being set
for A1 being SetSequence of X holds Partial_Union A1 is V75()

proof end;

theorem Th12: :: PROB_3:12

for n being Nat
for X being set
for A1 being SetSequence of X
for x being object holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )

proof end;

theorem Th13: :: PROB_3:13

for n being Nat
for x being object
for X being set
for A1 being SetSequence of X holds
( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )

proof end;

theorem Th14: :: PROB_3:14

for X being set
for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1

proof end;

theorem Th15: :: PROB_3:15

for X being set
for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1

proof end;

definition

let X be set ;
let A1 be SetSequence of X;

func Partial_Diff_Union A1 -> SetSequence of X means :Def3: :: PROB_3:def 3
( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) );

existence
ex b₁ being SetSequence of X st
( b₁ . 0 = A1 . 0 & ( for n being Nat holds b₁ . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of X st b₁ . 0 = A1 . 0 & ( for n being Nat holds b₁ . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) & b₂ . 0 = A1 . 0 & ( for n being Nat holds b₂ . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Partial_Diff_Union A1 iff ( b₃ . 0 = A1 . 0 & ( for n being Nat holds b₃ . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) );

theorem Th16: :: PROB_3:16

for n being Nat
for x being object
for X being set
for A1 being SetSequence of X holds
( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) )

proof end;

theorem Th17: :: PROB_3:17

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n by Th16;

theorem Th18: :: PROB_3:18

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n

proof end;

theorem Th19: :: PROB_3:19

for X being set
for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1

proof end;

theorem Th20: :: PROB_3:20

for X being set
for A1 being SetSequence of X holds Union (Partial_Diff_Union A1) = Union A1

proof end;

definition

let X be set ;
let A1 be SetSequence of X;

:: original: disjoint_valued
redefine attr A1 is disjoint_valued means :: PROB_3:def 4
for m, n being Nat st m <> n holds
A1 . m misses A1 . n;

compatibility
( A1 is disjoint_valued iff for m, n being Nat st m <> n holds
A1 . m misses A1 . n )

proof end;

end;

:: deftheorem defines disjoint_valued PROB_3:def 4 :
for X being set
for A1 being SetSequence of X holds
( A1 is disjoint_valued iff for m, n being Nat st m <> n holds
A1 . m misses A1 . n );

registration

let X be set ;
let A1 be SetSequence of X;

cluster Partial_Diff_Union A1 -> V77() ;

coherence
Partial_Diff_Union A1 is disjoint_valued

proof end;

end;

registration

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;

cluster Partial_Intersection XSeq -> Si -valued ;

coherence
Partial_Intersection XSeq is Si -valued

proof end;

end;

registration

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;

cluster Partial_Union XSeq -> Si -valued ;

coherence
Partial_Union XSeq is Si -valued

proof end;

end;

registration

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;

cluster Partial_Diff_Union XSeq -> Si -valued ;

coherence
Partial_Diff_Union XSeq is Si -valued

proof end;

end;

theorem :: PROB_3:21

for X being set
for Si being SigmaField of X
for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Intersection XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) /\ (XSeq . (n + 1)) ) ) by Def1;

theorem :: PROB_3:22

for X being set
for Si being SigmaField of X
for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Union XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) \/ (XSeq . (n + 1)) ) ) by Def2;

theorem :: PROB_3:23

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Intersection XSeq) . n c= XSeq . n by Th8;

theorem :: PROB_3:24

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds XSeq . n c= (Partial_Union XSeq) . n by Th9;

theorem :: PROB_3:25

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si
for x being object holds
( x in (Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds
x in XSeq . k )

proof end;

theorem :: PROB_3:26

for n being Nat
for x being object
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )

proof end;

theorem :: PROB_3:27

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Partial_Intersection XSeq is V74() by Th10;

theorem :: PROB_3:28

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Partial_Union XSeq is V75() by Th11;

theorem :: PROB_3:29

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Intersection (Partial_Intersection XSeq) = Intersection XSeq by Th14;

theorem :: PROB_3:30

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (Partial_Union XSeq) = Union XSeq by Th15;

theorem :: PROB_3:31

for X being set
for Si being SigmaField of X
for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Diff_Union XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (XSeq . (n + 1)) \ ((Partial_Union XSeq) . n) ) ) by Def3;

theorem :: PROB_3:32

for n being Nat
for x being object
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds
not x in XSeq . k ) ) )

proof end;

theorem :: PROB_3:33

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= XSeq . n by Th17;

theorem :: PROB_3:34

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= (Partial_Union XSeq) . n by Th18;

theorem :: PROB_3:35

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19;

theorem :: PROB_3:36

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (Partial_Diff_Union XSeq) = Union XSeq by Th20;

theorem Th37: :: PROB_3:37

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing

proof end;

theorem :: PROB_3:38

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing

proof end;

theorem :: PROB_3:39

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

proof end;

theorem Th40: :: PROB_3:40

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

proof end;

theorem Th41: :: PROB_3:41

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( P * (Partial_Union ASeq) is convergent & lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) & lim (P * (Partial_Union ASeq)) = P . (Union ASeq) )

proof end;

theorem Th42: :: PROB_3:42

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma st ASeq is V77() holds
for n, m being Nat st n < m holds
(Partial_Union ASeq) . n misses ASeq . m

proof end;

theorem Th43: :: PROB_3:43

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V77() holds
(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

proof end;

theorem Th44: :: PROB_3:44

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V77() holds
P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th43;

theorem Th45: :: PROB_3:45

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V77() holds
( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

proof end;

theorem Th46: :: PROB_3:46

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V77() holds
P . (Union ASeq) = Sum (P * ASeq)

proof end;

definition

let X be set ;
let F1 be FinSequence of bool X;
let n be Nat;
:: original: .
redefine func F1 . n -> Subset of X;
coherence
F1 . n is Subset of X

proof end;

end;

theorem :: PROB_3:47

for X being set ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X

proof end;

theorem :: PROB_3:48

for X being set
for F1 being FinSequence of bool X holds union (rng F1) is Subset of X ;

definition

let X be set ;
let F1 be FinSequence of bool X;
:: original: Union
redefine func Union F1 -> Subset of X;
coherence
Union F1 is Subset of X

proof end;

end;

theorem Th49: :: PROB_3:49

for x being object
for X being set
for F1 being FinSequence of bool X holds
( x in Union F1 iff ex k being Nat st
( k in dom F1 & x in F1 . k ) )

proof end;

definition

let X be set ;
let F1 be FinSequence of bool X;

func Complement F1 -> FinSequence of bool X means :Def5: :: PROB_3:def 5
( len it = len F1 & ( for n being Nat st n in dom it holds
it . n = (F1 . n) ` ) );

existence
ex b₁ being FinSequence of bool X st
( len b₁ = len F1 & ( for n being Nat st n in dom b₁ holds
b₁ . n = (F1 . n) ` ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of bool X st len b₁ = len F1 & ( for n being Nat st n in dom b₁ holds
b₁ . n = (F1 . n) ` ) & len b<sub>2</sub> = len F1 & ( for n being Nat st n in dom b<sub>2</sub> holds
b<sub>2</sub> . n = (F1 . n) ` ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Complement PROB_3:def 5 :
for X being set
for F1, b₃ being FinSequence of bool X holds
( b₃ = Complement F1 iff ( len b₃ = len F1 & ( for n being Nat st n in dom b₃ holds
b₃ . n = (F1 . n) ` ) ) );

definition

let X be set ;
let F1 be FinSequence of bool X;

func Intersection F1 -> Subset of X equals :Def6: :: PROB_3:def 6
(Union (Complement F1)) ` if F1 <> {}
otherwise {} ;

coherence
( ( F1 <> {} implies (Union (Complement F1)) ` is Subset of X ) & ( not F1 <> {} implies {} is Subset of X ) ) by SUBSET_1:1;
consistency
for b₁ being Subset of X holds verum ;

end;

:: deftheorem Def6 defines Intersection PROB_3:def 6 :
for X being set
for F1 being FinSequence of bool X holds
( ( F1 <> {} implies Intersection F1 = (Union (Complement F1)) ` ) & ( not F1 <> {} implies Intersection F1 = {} ) );

theorem Th50: :: PROB_3:50

for X being set
for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1

proof end;

theorem Th51: :: PROB_3:51

for X being set
for F1 being FinSequence of bool X
for x being object st F1 <> {} holds
( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )

proof end;

theorem Th52: :: PROB_3:52

for x being object
for X being set
for F1 being FinSequence of bool X st F1 <> {} holds
( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n )

proof end;

theorem :: PROB_3:53

for X being set
for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)

proof end;

theorem Th54: :: PROB_3:54

for X being set
for F1 being FinSequence of bool X ex A1 being SetSequence of X st
( ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) )

proof end;

theorem Th55: :: PROB_3:55

for X being set
for F1 being FinSequence of bool X
for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) holds
( A1 . 0 = {} & Union A1 = Union F1 )

proof end;

definition

let X be set ;
let Si be SigmaField of X;
:: original: FinSequence
redefine mode FinSequence of Si -> FinSequence of bool X;
coherence
for b₁ being FinSequence of Si holds b₁ is FinSequence of bool X

proof end;

end;

definition

let X be set ;
let Si be SigmaField of X;
let FSi be FinSequence of Si;
let n be Nat;
:: original: .
redefine func FSi . n -> Event of Si;
coherence
FSi . n is Event of Si

proof end;

end;

theorem Th56: :: PROB_3:56

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si ex ASeq being SetSequence of Si st
( ( for k being Nat st k in dom FSi holds
ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds
ASeq . k = {} ) )

proof end;

theorem Th57: :: PROB_3:57

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si holds Union FSi in Si

proof end;

registration

let X be set ;
let S be SigmaField of X;
let F be FinSequence of S;

cluster Complement F -> S -valued ;

coherence
Complement F is S -valued

proof end;

end;

theorem :: PROB_3:58

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si holds Intersection FSi in Si

proof end;

theorem Th59: :: PROB_3:59

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

proof end;

theorem Th60: :: PROB_3:60

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let FSeq be FinSequence of Sigma;
let P be Probability of Sigma;
:: original: *
redefine func P * FSeq -> FinSequence of REAL ;
coherence
FSeq * P is FinSequence of REAL by Th60;

end;

theorem Th61: :: PROB_3:61

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

proof end;

theorem Th62: :: PROB_3:62

for RFin being FinSequence of REAL st len RFin = 0 holds
Sum RFin = 0

proof end;

theorem Th63: :: PROB_3:63

for RFin being FinSequence of REAL st len RFin >= 1 holds
ex f being Real_Sequence st
( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) )

proof end;

theorem Th64: :: PROB_3:64

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma
for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds
ASeq . k = {} ) holds
( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) & P . (Union ASeq) <= Sum (P * ASeq) & Sum (P * FSeq) = Sum (P * ASeq) )

proof end;

theorem :: PROB_3:65

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )

proof end;

definition

let X be set ;
let IT be Subset-Family of X;

attr IT is non-decreasing-closed means :Def7: :: PROB_3:def 9
for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds
Union A1 in IT;

attr IT is non-increasing-closed means :Def8: :: PROB_3:def 10
for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
Intersection A1 in IT;

end;

:: deftheorem PROB_3:def 7 :
canceled;

:: deftheorem PROB_3:def 8 :
canceled;

:: deftheorem Def7 defines non-decreasing-closed PROB_3:def 9 :
for X being set
for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds
Union A1 in IT );

:: deftheorem Def8 defines non-increasing-closed PROB_3:def 10 :
for X being set
for IT being Subset-Family of X holds
( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
Intersection A1 in IT );

theorem Th66: :: PROB_3:66

for X being set
for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds
lim A1 in IT )

proof end;

theorem Th67: :: PROB_3:67

for X being set
for IT being Subset-Family of X holds
( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
lim A1 in IT )

proof end;

theorem Th68: :: PROB_3:68

for X being set holds
( bool X is non-decreasing-closed & bool X is non-increasing-closed ) ;

registration

let X be set ;

cluster non-decreasing-closed non-increasing-closed for Element of K10(K10(X));

existence
ex b₁ being Subset-Family of X st
( b₁ is non-decreasing-closed & b₁ is non-increasing-closed )

proof end;

end;

definition

let X be set ;
mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X;

end;

theorem Th69: :: PROB_3:69

for X, Z being set holds
( Z is MonotoneClass of X iff ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) )

proof end;

theorem Th70: :: PROB_3:70

for X being set
for F being Field_Subset of X holds
( F is SigmaField of X iff F is MonotoneClass of X )

proof end;

theorem :: PROB_3:71

for Omega being non empty set holds bool Omega is MonotoneClass of Omega by Th68;

definition

let Omega be non empty set ;
let X be Subset-Family of Omega;

func monotoneclass X -> MonotoneClass of Omega means :Def9: :: PROB_3:def 11
( X c= it & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
it c= Z ) );

existence
ex b₁ being MonotoneClass of Omega st
( X c= b₁ & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b₁ c= Z ) )

proof end;

uniqueness
for b₁, b₂ being MonotoneClass of Omega st X c= b₁ & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b₁ c= Z ) & X c= b₂ & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b₂ c= Z ) holds
b₁ = b₂ ;

end;

:: deftheorem Def9 defines monotoneclass PROB_3:def 11 :
for Omega being non empty set
for X being Subset-Family of Omega
for b₃ being MonotoneClass of Omega holds
( b₃ = monotoneclass X iff ( X c= b₃ & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b₃ c= Z ) ) );

theorem Th72: :: PROB_3:72

for Omega being non empty set
for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega

proof end;

theorem :: PROB_3:73

for Omega being non empty set
for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z

proof end;