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


begin

Lm1: for t, p, s being real number 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 number
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 V71() 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 V70() 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 b1 being SetSequence of X st
( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) /\ (A1 . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) /\ (A1 . (n + 1)) ) & b2 . 0 = A1 . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) /\ (A1 . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :
for X being set
for A1, b3 being SetSequence of X holds
( b3 = Partial_Intersection A1 iff ( b3 . 0 = A1 . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . 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 b1 being SetSequence of X st
( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (A1 . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (A1 . (n + 1)) ) & b2 . 0 = A1 . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) \/ (A1 . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :
for X being set
for A1, b3 being SetSequence of X holds
( b3 = Partial_Union A1 iff ( b3 . 0 = A1 . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . 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 V70()
proof end;

theorem Th11: :: PROB_3:11
for X being set
for A1 being SetSequence of X holds Partial_Union A1 is V71()
proof end;

theorem Th12: :: PROB_3:12
for n being Nat
for X, x being set
for A1 being SetSequence of X 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, 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 b1 being SetSequence of X st
( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) & b2 . 0 = A1 . 0 & ( for n being Nat holds b2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) holds
b1 = b2
proof end;
end;

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

theorem Th16: :: PROB_3:16
for n being Nat
for X, 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
proof end;

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 :Def4: :: 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 Def4 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 -> V73() ;
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 YSeq, XSeq 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 YSeq, XSeq 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, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds
x in XSeq . k ) by Th12;

theorem :: PROB_3:26
for n being Nat
for X, 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 ) ) by Th13;

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 V70() 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 V71() 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 YSeq, XSeq 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, 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 ) ) ) by Th16;

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 V73() 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 V73() 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 V73() holds
P * (Partial_Union ASeq) = Partial_Sums (P * ASeq)
proof end;

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 V73() 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 V73() 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, 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 b1 being FinSequence of bool X st
( len b1 = len F1 & ( for n being Nat st n in dom b1 holds
b1 . n = (F1 . n) ` ) )
proof end;
uniqueness
for b1, b2 being FinSequence of bool X st len b1 = len F1 & ( for n being Nat st n in dom b1 holds
b1 . n = (F1 . n) ` ) & len b2 = len F1 & ( for n being Nat st n in dom b2 holds
b2 . n = (F1 . n) ` ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Complement PROB_3:def 5 :
for X being set
for F1, b3 being FinSequence of bool X holds
( b3 = Complement F1 iff ( len b3 = len F1 & ( for n being Nat st n in dom b3 holds
b3 . 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 b1 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, x being set
for F1 being FinSequence of bool X 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, 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 b1 being FinSequence of Si holds b1 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
canceled;
canceled;
let X be set ;
let IT be Subset-Family of X;
attr IT is non-decreasing-closed means :Def9: :: PROB_3:def 9
for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
Union A1 in IT;
attr IT is non-increasing-closed means :Def10: :: PROB_3:def 10
for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
Intersection A1 in IT;
end;

:: deftheorem PROB_3:def 7 :
canceled;

:: deftheorem PROB_3:def 8 :
canceled;

:: deftheorem Def9 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 V71() & rng A1 c= IT holds
Union A1 in IT );

:: deftheorem Def10 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 V70() & 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 V71() & 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 V70() & 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 )
proof end;

registration
let X be set ;
cluster non-decreasing-closed non-increasing-closed for Element of K10(K10(X));
existence
ex b1 being Subset-Family of X st
( b1 is non-decreasing-closed & b1 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 Z, X 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 :Def11: :: 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 b1 being MonotoneClass of Omega st
( X c= b1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b1 c= Z ) )
proof end;
uniqueness
for b1, b2 being MonotoneClass of Omega st X c= b1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b1 c= Z ) & X c= b2 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b2 c= Z ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines monotoneclass PROB_3:def 11 :
for Omega being non empty set
for X being Subset-Family of Omega
for b3 being MonotoneClass of Omega holds
( b3 = monotoneclass X iff ( X c= b3 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b3 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;