:: PROB_3 semantic presentation
begin
Lm1: for t, p, s being real number st 0 < s & t <= p holds
( t < p + s & t - s < p )
proof
let t, p, s be real number ; ::_thesis: ( 0 < s & t <= p implies ( t < p + s & t - s < p ) )
assume ( 0 < s & t <= p ) ; ::_thesis: ( t < p + s & t - s < p )
then t + 0 < p + s by XREAL_1:8;
hence ( t < p + s & t - s < p ) by XREAL_1:19; ::_thesis: verum
end;
theorem Th1: :: PROB_3:1
for f being FinSequence holds not 0 in dom f
proof
let f be FinSequence; ::_thesis: not 0 in dom f
assume 0 in dom f ; ::_thesis: contradiction
then 0 in Seg (len f) by FINSEQ_1:def_3;
hence contradiction by FINSEQ_1:1; ::_thesis: verum
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
let n be Nat; ::_thesis: for f being FinSequence holds
( n in dom f iff ( n <> 0 & n <= len f ) )
let f be FinSequence; ::_thesis: ( n in dom f iff ( n <> 0 & n <= len f ) )
( n in dom f iff ( n >= 1 & n <= len f ) ) by FINSEQ_3:25;
hence ( n in dom f iff ( n <> 0 & n <= len f ) ) by NAT_1:14; ::_thesis: verum
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
let g be real number ; ::_thesis: 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 )
let f be Real_Sequence; ::_thesis: ( ex k being Nat st
for n being Nat st k <= n holds
f . n = g implies ( f is convergent & lim f = g ) )
given k being Nat such that A1: for n being Nat st k <= n holds
f . n = g ; ::_thesis: ( f is convergent & lim f = g )
A2: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_k1_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k1_<=_m_holds_
abs_((f_._m)_-_g)_<_p
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
let p be real number ; ::_thesis: ( 0 < p implies ex k1 being Element of NAT st
for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p )
assume A3: 0 < p ; ::_thesis: ex k1 being Element of NAT st
for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p
take k1 = k1; ::_thesis: for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p
thus for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( k1 <= m implies abs ((f . m) - g) < p )
assume k1 <= m ; ::_thesis: abs ((f . m) - g) < p
then f . m = g by A1;
hence abs ((f . m) - g) < p by A3, ABSVALUE:2; ::_thesis: verum
end;
end;
hence f is convergent by SEQ_2:def_6; ::_thesis: lim f = g
hence lim f = g by A2, SEQ_2:def_7; ::_thesis: verum
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
let n be Nat; ::_thesis: 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
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * ASeq) . n >= 0
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * ASeq) . n >= 0
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds (P * ASeq) . n >= 0
let P be Probability of Sigma; ::_thesis: (P * ASeq) . n >= 0
A1: n in NAT by ORDINAL1:def_12;
then A2: ASeq . n is Event of Sigma by PROB_1:25;
dom (P * ASeq) = NAT by SEQ_1:1;
then (P * ASeq) . n = P . (ASeq . n) by A1, FUNCT_1:12;
hence (P * ASeq) . n >= 0 by A2, PROB_1:def_8; ::_thesis: verum
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
let n be Nat; ::_thesis: 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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: 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
let ASeq, BSeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq . n c= BSeq . n holds
(P * ASeq) . n <= (P * BSeq) . n
let P be Probability of Sigma; ::_thesis: ( ASeq . n c= BSeq . n implies (P * ASeq) . n <= (P * BSeq) . n )
A1: n in NAT by ORDINAL1:def_12;
A2: ( ASeq . n in rng ASeq & BSeq . n in rng BSeq ) by NAT_1:51;
assume ASeq . n c= BSeq . n ; ::_thesis: (P * ASeq) . n <= (P * BSeq) . n
then P . (ASeq . n) <= P . (BSeq . n) by A2, PROB_1:34;
then (P * ASeq) . n <= P . (BSeq . n) by A1, FUNCT_2:15;
hence (P * ASeq) . n <= (P * BSeq) . n by A1, FUNCT_2:15; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V71() holds
P * ASeq is non-decreasing
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V71() holds
P * ASeq is non-decreasing
let P be Probability of Sigma; ::_thesis: ( ASeq is V71() implies P * ASeq is non-decreasing )
A1: dom (P * ASeq) = NAT by SEQ_1:1;
assume A2: ASeq is V71() ; ::_thesis: P * ASeq is non-decreasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_
(P_*_ASeq)_._n_<=_(P_*_ASeq)_._m
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (P * ASeq) . n <= (P * ASeq) . m )
assume n <= m ; ::_thesis: (P * ASeq) . n <= (P * ASeq) . m
then A3: ASeq . n c= ASeq . m by A2, PROB_1:def_5;
( (P * ASeq) . n = P . (ASeq . n) & (P * ASeq) . m = P . (ASeq . m) ) by A1, FUNCT_1:12;
hence (P * ASeq) . n <= (P * ASeq) . m by A3, PROB_1:34; ::_thesis: verum
end;
hence P * ASeq is non-decreasing by SEQM_3:6; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V70() holds
P * ASeq is non-increasing
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V70() holds
P * ASeq is non-increasing
let P be Probability of Sigma; ::_thesis: ( ASeq is V70() implies P * ASeq is non-increasing )
A1: dom (P * ASeq) = NAT by SEQ_1:1;
assume A2: ASeq is V70() ; ::_thesis: P * ASeq is non-increasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_
(P_*_ASeq)_._m_<=_(P_*_ASeq)_._n
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (P * ASeq) . m <= (P * ASeq) . n )
assume n <= m ; ::_thesis: (P * ASeq) . m <= (P * ASeq) . n
then A3: ASeq . m c= ASeq . n by A2, PROB_1:def_4;
( (P * ASeq) . n = P . (ASeq . n) & (P * ASeq) . m = P . (ASeq . m) ) by A1, FUNCT_1:12;
hence (P * ASeq) . m <= (P * ASeq) . n by A3, PROB_1:34; ::_thesis: verum
end;
hence P * ASeq is non-increasing by SEQM_3:8; ::_thesis: verum
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
defpred S1[ set , set , set ] means for x, y being Subset of X
for s being Nat st s = $1 & x = $2 & y = $3 holds
y = x /\ (A1 . (s + 1));
A1: for n being Element of NAT
for x being Subset of X ex y being Subset of X st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y]
let x be Subset of X; ::_thesis: ex y being Subset of X st S1[n,x,y]
take x /\ (A1 . (n + 1)) ; ::_thesis: S1[n,x,x /\ (A1 . (n + 1))]
thus S1[n,x,x /\ (A1 . (n + 1))] ; ::_thesis: verum
end;
consider F being SetSequence of X such that
A2: F . 0 = A1 . 0 and
A3: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A1);
take F ; ::_thesis: ( F . 0 = A1 . 0 & ( for n being Nat holds F . (n + 1) = (F . n) /\ (A1 . (n + 1)) ) )
thus F . 0 = A1 . 0 by A2; ::_thesis: for n being Nat holds F . (n + 1) = (F . n) /\ (A1 . (n + 1))
let n be Nat; ::_thesis: F . (n + 1) = (F . n) /\ (A1 . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def_12;
S1[n,F . n,F . (n + 1)] by A3;
hence F . (n + 1) = (F . n) /\ (A1 . (n + 1)) ; ::_thesis: verum
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
let S1, S2 be SetSequence of X; ::_thesis: ( S1 . 0 = A1 . 0 & ( for n being Nat holds S1 . (n + 1) = (S1 . n) /\ (A1 . (n + 1)) ) & S2 . 0 = A1 . 0 & ( for n being Nat holds S2 . (n + 1) = (S2 . n) /\ (A1 . (n + 1)) ) implies S1 = S2 )
assume that
A4: S1 . 0 = A1 . 0 and
A5: for n being Nat holds S1 . (n + 1) = (S1 . n) /\ (A1 . (n + 1)) and
A6: S2 . 0 = A1 . 0 and
A7: for n being Nat holds S2 . (n + 1) = (S2 . n) /\ (A1 . (n + 1)) ; ::_thesis: S1 = S2
defpred S1[ set ] means S1 . $1 = S2 . $1;
for n being set st n in NAT holds
S1[n]
proof
let n be set ; ::_thesis: ( n in NAT implies S1[n] )
assume n in NAT ; ::_thesis: S1[n]
then reconsider n = n as Element of NAT ;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1 . k = S2 . k ; ::_thesis: S1[k + 1]
hence S1 . (k + 1) = (S2 . k) /\ (A1 . (k + 1)) by A5
.= S2 . (k + 1) by A7 ;
::_thesis: verum
end;
A9: S1[ 0 ] by A4, A6;
for k being Nat holds S1[k] from NAT_1:sch_2(A9, A8);
then S1 . n = S2 . n ;
hence S1[n] ; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:12; ::_thesis: verum
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
defpred S1[ set , set , set ] means for x, y being Subset of X
for s being Nat st s = $1 & x = $2 & y = $3 holds
y = x \/ (A1 . (s + 1));
A1: for n being Element of NAT
for x being Subset of X ex y being Subset of X st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y]
let x be Subset of X; ::_thesis: ex y being Subset of X st S1[n,x,y]
take x \/ (A1 . (n + 1)) ; ::_thesis: S1[n,x,x \/ (A1 . (n + 1))]
thus S1[n,x,x \/ (A1 . (n + 1))] ; ::_thesis: verum
end;
consider F being SetSequence of X such that
A2: F . 0 = A1 . 0 and
A3: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A1);
take F ; ::_thesis: ( F . 0 = A1 . 0 & ( for n being Nat holds F . (n + 1) = (F . n) \/ (A1 . (n + 1)) ) )
thus F . 0 = A1 . 0 by A2; ::_thesis: for n being Nat holds F . (n + 1) = (F . n) \/ (A1 . (n + 1))
let n be Nat; ::_thesis: F . (n + 1) = (F . n) \/ (A1 . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def_12;
S1[n,F . n,F . (n + 1)] by A3;
hence F . (n + 1) = (F . n) \/ (A1 . (n + 1)) ; ::_thesis: verum
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
let S1, S2 be SetSequence of X; ::_thesis: ( S1 . 0 = A1 . 0 & ( for n being Nat holds S1 . (n + 1) = (S1 . n) \/ (A1 . (n + 1)) ) & S2 . 0 = A1 . 0 & ( for n being Nat holds S2 . (n + 1) = (S2 . n) \/ (A1 . (n + 1)) ) implies S1 = S2 )
assume that
A4: S1 . 0 = A1 . 0 and
A5: for n being Nat holds S1 . (n + 1) = (S1 . n) \/ (A1 . (n + 1)) and
A6: S2 . 0 = A1 . 0 and
A7: for n being Nat holds S2 . (n + 1) = (S2 . n) \/ (A1 . (n + 1)) ; ::_thesis: S1 = S2
defpred S1[ set ] means S1 . $1 = S2 . $1;
for n being set st n in NAT holds
S1[n]
proof
let n be set ; ::_thesis: ( n in NAT implies S1[n] )
assume n in NAT ; ::_thesis: S1[n]
then reconsider n = n as Element of NAT ;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1 . k = S2 . k ; ::_thesis: S1[k + 1]
hence S1 . (k + 1) = (S2 . k) \/ (A1 . (k + 1)) by A5
.= S2 . (k + 1) by A7 ;
::_thesis: verum
end;
A9: S1[ 0 ] by A4, A6;
for k being Nat holds S1[k] from NAT_1:sch_2(A9, A8);
then S1 . n = S2 . n ;
hence S1[n] ; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:12; ::_thesis: verum
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
let n be Nat; ::_thesis: for X being set
for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n
let X be set ; ::_thesis: for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n
let A1 be SetSequence of X; ::_thesis: (Partial_Intersection A1) . n c= A1 . n
percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: (Partial_Intersection A1) . n c= A1 . n
hence (Partial_Intersection A1) . n c= A1 . n by Def1; ::_thesis: verum
end;
suppose ex k being Nat st n = k + 1 ; ::_thesis: (Partial_Intersection A1) . n c= A1 . n
then consider k being Nat such that
A1: n = k + 1 ;
(Partial_Intersection A1) . (k + 1) = ((Partial_Intersection A1) . k) /\ (A1 . (k + 1)) by Def1;
hence (Partial_Intersection A1) . n c= A1 . n by A1, XBOOLE_1:17; ::_thesis: verum
end;
end;
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
let n be Nat; ::_thesis: for X being set
for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n
let X be set ; ::_thesis: for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n
let A1 be SetSequence of X; ::_thesis: A1 . n c= (Partial_Union A1) . n
percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: A1 . n c= (Partial_Union A1) . n
hence A1 . n c= (Partial_Union A1) . n by Def2; ::_thesis: verum
end;
suppose ex k being Nat st n = k + 1 ; ::_thesis: A1 . n c= (Partial_Union A1) . n
then consider k being Nat such that
A1: n = k + 1 ;
(Partial_Union A1) . (k + 1) = ((Partial_Union A1) . k) \/ (A1 . (k + 1)) by Def2;
hence A1 . n c= (Partial_Union A1) . n by A1, XBOOLE_1:7; ::_thesis: verum
end;
end;
end;
theorem Th10: :: PROB_3:10
for X being set
for A1 being SetSequence of X holds Partial_Intersection A1 is V70()
proof
let X be set ; ::_thesis: for A1 being SetSequence of X holds Partial_Intersection A1 is V70()
let A1 be SetSequence of X; ::_thesis: Partial_Intersection A1 is V70()
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Intersection_A1)_._(n_+_1)_c=_(Partial_Intersection_A1)_._n
let n be Element of NAT ; ::_thesis: (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n
(Partial_Intersection A1) . (n + 1) = ((Partial_Intersection A1) . n) /\ (A1 . (n + 1)) by Def1;
hence (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n by XBOOLE_1:17; ::_thesis: verum
end;
hence Partial_Intersection A1 is V70() by PROB_2:6; ::_thesis: verum
end;
theorem Th11: :: PROB_3:11
for X being set
for A1 being SetSequence of X holds Partial_Union A1 is V71()
proof
let X be set ; ::_thesis: for A1 being SetSequence of X holds Partial_Union A1 is V71()
let A1 be SetSequence of X; ::_thesis: Partial_Union A1 is V71()
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Union_A1)_._n_c=_(Partial_Union_A1)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1)
(Partial_Union A1) . (n + 1) = ((Partial_Union A1) . n) \/ (A1 . (n + 1)) by Def2;
hence (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1) by XBOOLE_1:7; ::_thesis: verum
end;
hence Partial_Union A1 is V71() by PROB_2:7; ::_thesis: verum
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
let n be Nat; ::_thesis: 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 )
let X, x be set ; ::_thesis: 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 )
let A1 be SetSequence of X; ::_thesis: ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
defpred S1[ Nat] means ( ( for k being Nat st k <= $1 holds
x in A1 . k ) implies x in (Partial_Intersection A1) . $1 );
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: ( ( for k being Nat st k <= i holds
x in A1 . k ) implies x in (Partial_Intersection A1) . i ) ; ::_thesis: S1[i + 1]
assume for k being Nat st k <= i + 1 holds
x in A1 . k ; ::_thesis: x in (Partial_Intersection A1) . (i + 1)
then A3: ( ( for k being Nat st k <= i holds
x in A1 . k ) & x in A1 . (i + 1) ) by NAT_1:12;
(Partial_Intersection A1) . (i + 1) = ((Partial_Intersection A1) . i) /\ (A1 . (i + 1)) by Def1;
hence x in (Partial_Intersection A1) . (i + 1) by A2, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
thus ( x in (Partial_Intersection A1) . n implies for k being Nat st k <= n holds
x in A1 . k ) ::_thesis: ( ( for k being Nat st k <= n holds
x in A1 . k ) implies x in (Partial_Intersection A1) . n )
proof
assume A4: x in (Partial_Intersection A1) . n ; ::_thesis: for k being Nat st k <= n holds
x in A1 . k
for k being Nat st k <= n holds
x in A1 . k
proof
A5: Partial_Intersection A1 is V70() by Th10;
let k be Nat; ::_thesis: ( k <= n implies x in A1 . k )
assume A6: k <= n ; ::_thesis: x in A1 . k
A7: (Partial_Intersection A1) . k c= A1 . k by Th8;
( n in NAT & k in NAT ) by ORDINAL1:def_12;
then (Partial_Intersection A1) . n c= (Partial_Intersection A1) . k by A6, A5, PROB_1:def_4;
then (Partial_Intersection A1) . n c= A1 . k by A7, XBOOLE_1:1;
hence x in A1 . k by A4; ::_thesis: verum
end;
hence for k being Nat st k <= n holds
x in A1 . k ; ::_thesis: verum
end;
A8: S1[ 0 ]
proof
assume for k being Nat st k <= 0 holds
x in A1 . k ; ::_thesis: x in (Partial_Intersection A1) . 0
then x in A1 . 0 ;
hence x in (Partial_Intersection A1) . 0 by Def1; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A8, A1);
hence ( ( for k being Nat st k <= n holds
x in A1 . k ) implies x in (Partial_Intersection A1) . n ) ; ::_thesis: verum
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
let n be Nat; ::_thesis: 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 ) )
let X, x be set ; ::_thesis: 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 ) )
let A1 be SetSequence of X; ::_thesis: ( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )
defpred S1[ Nat] means ( x in (Partial_Union A1) . $1 implies ex k being Nat st
( k <= $1 & x in A1 . k ) );
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: ( x in (Partial_Union A1) . i implies ex k being Nat st
( k <= i & x in A1 . k ) ) ; ::_thesis: S1[i + 1]
assume A3: x in (Partial_Union A1) . (i + 1) ; ::_thesis: ex k being Nat st
( k <= i + 1 & x in A1 . k )
A4: (Partial_Union A1) . (i + 1) = ((Partial_Union A1) . i) \/ (A1 . (i + 1)) by Def2;
now__::_thesis:_(_(_x_in_(Partial_Union_A1)_._i_&_ex_k,_k_being_Nat_st_
(_k_<=_i_+_1_&_x_in_A1_._k_)_)_or_(_x_in_A1_._(i_+_1)_&_ex_k_being_Nat_st_
(_k_<=_i_+_1_&_x_in_A1_._k_)_)_)
percases ( x in (Partial_Union A1) . i or x in A1 . (i + 1) ) by A3, A4, XBOOLE_0:def_3;
case x in (Partial_Union A1) . i ; ::_thesis: ex k, k being Nat st
( k <= i + 1 & x in A1 . k )
then consider k being Nat such that
A5: ( k <= i & x in A1 . k ) by A2;
take k = k; ::_thesis: ex k being Nat st
( k <= i + 1 & x in A1 . k )
thus ex k being Nat st
( k <= i + 1 & x in A1 . k ) by A5, NAT_1:12; ::_thesis: verum
end;
case x in A1 . (i + 1) ; ::_thesis: ex k being Nat st
( k <= i + 1 & x in A1 . k )
hence ex k being Nat st
( k <= i + 1 & x in A1 . k ) ; ::_thesis: verum
end;
end;
end;
hence ex k being Nat st
( k <= i + 1 & x in A1 . k ) ; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
assume A7: x in (Partial_Union A1) . 0 ; ::_thesis: ex k being Nat st
( k <= 0 & x in A1 . k )
take 0 ; ::_thesis: ( 0 <= 0 & x in A1 . 0 )
thus ( 0 <= 0 & x in A1 . 0 ) by A7, Def2; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A6, A1);
hence ( x in (Partial_Union A1) . n implies ex k being Nat st
( k <= n & x in A1 . k ) ) ; ::_thesis: ( ex k being Nat st
( k <= n & x in A1 . k ) implies x in (Partial_Union A1) . n )
given i being Nat such that A8: i <= n and
A9: x in A1 . i ; ::_thesis: x in (Partial_Union A1) . n
A1 . i c= (Partial_Union A1) . i by Th9;
then A10: x in (Partial_Union A1) . i by A9;
A11: Partial_Union A1 is V71() by Th11;
( n in NAT & i in NAT ) by ORDINAL1:def_12;
then (Partial_Union A1) . i c= (Partial_Union A1) . n by A8, A11, PROB_1:def_5;
hence x in (Partial_Union A1) . n by A10; ::_thesis: verum
end;
theorem Th14: :: PROB_3:14
for X being set
for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1
proof
let X be set ; ::_thesis: for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1
let A1 be SetSequence of X; ::_thesis: Intersection (Partial_Intersection A1) = Intersection A1
thus Intersection (Partial_Intersection A1) c= Intersection A1 :: according to XBOOLE_0:def_10 ::_thesis: Intersection A1 c= Intersection (Partial_Intersection A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (Partial_Intersection A1) or x in Intersection A1 )
assume A1: x in Intersection (Partial_Intersection A1) ; ::_thesis: x in Intersection A1
for n being Element of NAT holds x in A1 . n
proof
let n be Element of NAT ; ::_thesis: x in A1 . n
x in (Partial_Intersection A1) . n by A1, PROB_1:13;
hence x in A1 . n by Th12; ::_thesis: verum
end;
hence x in Intersection A1 by PROB_1:13; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection A1 or x in Intersection (Partial_Intersection A1) )
assume A2: x in Intersection A1 ; ::_thesis: x in Intersection (Partial_Intersection A1)
for n being Element of NAT holds x in (Partial_Intersection A1) . n
proof
let n be Element of NAT ; ::_thesis: x in (Partial_Intersection A1) . n
for k being Nat st k <= n holds
x in A1 . k
proof
let k be Nat; ::_thesis: ( k <= n implies x in A1 . k )
k in NAT by ORDINAL1:def_12;
hence ( k <= n implies x in A1 . k ) by A2, PROB_1:13; ::_thesis: verum
end;
hence x in (Partial_Intersection A1) . n by Th12; ::_thesis: verum
end;
hence x in Intersection (Partial_Intersection A1) by PROB_1:13; ::_thesis: verum
end;
theorem Th15: :: PROB_3:15
for X being set
for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1
proof
let X be set ; ::_thesis: for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1
let A1 be SetSequence of X; ::_thesis: Union (Partial_Union A1) = Union A1
thus Union (Partial_Union A1) c= Union A1 :: according to XBOOLE_0:def_10 ::_thesis: Union A1 c= Union (Partial_Union A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (Partial_Union A1) or x in Union A1 )
assume x in Union (Partial_Union A1) ; ::_thesis: x in Union A1
then consider n being Element of NAT such that
A1: x in (Partial_Union A1) . n by PROB_1:12;
consider k being Nat such that
k <= n and
A2: x in A1 . k by A1, Th13;
k in NAT by ORDINAL1:def_12;
hence x in Union A1 by A2, PROB_1:12; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union A1 or x in Union (Partial_Union A1) )
assume x in Union A1 ; ::_thesis: x in Union (Partial_Union A1)
then consider n being Element of NAT such that
A3: x in A1 . n by PROB_1:12;
x in (Partial_Union A1) . n by A3, Th13;
hence x in Union (Partial_Union A1) by PROB_1:12; ::_thesis: verum
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
defpred S1[ set , set , set ] means for x, y being Subset of X
for s being Nat st s = $1 & x = $2 & y = $3 holds
y = (A1 . (s + 1)) \ ((Partial_Union A1) . s);
set A = A1 . 0;
A1: for n being Element of NAT
for x being Subset of X ex y being Subset of X st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y]
let x be Subset of X; ::_thesis: ex y being Subset of X st S1[n,x,y]
take (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; ::_thesis: S1[n,x,(A1 . (n + 1)) \ ((Partial_Union A1) . n)]
thus S1[n,x,(A1 . (n + 1)) \ ((Partial_Union A1) . n)] ; ::_thesis: verum
end;
consider F being SetSequence of X such that
A2: ( F . 0 = A1 . 0 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
for n being Nat holds F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n)
proof
let n be Nat; ::_thesis: F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
for x, y being Subset of X
for s being Nat st s = n1 & x = F . n1 & y = F . (n1 + 1) holds
y = (A1 . (s + 1)) \ ((Partial_Union A1) . s) by A2;
hence F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; ::_thesis: verum
end;
hence 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) ) ) by A2; ::_thesis: verum
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
let S1, S2 be SetSequence of X; ::_thesis: ( S1 . 0 = A1 . 0 & ( for n being Nat holds S1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) & S2 . 0 = A1 . 0 & ( for n being Nat holds S2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) implies S1 = S2 )
assume that
A3: S1 . 0 = A1 . 0 and
A4: for n being Nat holds S1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) and
A5: S2 . 0 = A1 . 0 and
A6: for n being Nat holds S2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; ::_thesis: S1 = S2
defpred S1[ set ] means S1 . $1 = S2 . $1;
for n being set st n in NAT holds
S1[n]
proof
let n be set ; ::_thesis: ( n in NAT implies S1[n] )
assume n in NAT ; ::_thesis: S1[n]
then reconsider n = n as Element of NAT ;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1 . k = S2 . k ; ::_thesis: S1[k + 1]
thus S1 . (k + 1) = (A1 . (k + 1)) \ ((Partial_Union A1) . k) by A4
.= S2 . (k + 1) by A6 ; ::_thesis: verum
end;
A8: S1[ 0 ] by A3, A5;
for k being Nat holds S1[k] from NAT_1:sch_2(A8, A7);
then S1 . n = S2 . n ;
hence S1[n] ; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:12; ::_thesis: verum
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
let n be Nat; ::_thesis: 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 ) ) )
let X, x be set ; ::_thesis: 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 ) ) )
let A1 be SetSequence of X; ::_thesis: ( 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 ) ) )
thus ( x in (Partial_Diff_Union A1) . n implies ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) ) ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) implies x in (Partial_Diff_Union A1) . n )
proof
assume A1: x in (Partial_Diff_Union A1) . n ; ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) )
now__::_thesis:_(_(_n_=_0_&_x_in_A1_._n_&_(_for_k_being_Nat_st_k_<_n_holds_
not_x_in_A1_._k_)_)_or_(_ex_n1_being_Nat_st_n_=_n1_+_1_&_x_in_A1_._n_&_(_for_k_being_Nat_st_k_<_n_holds_
not_x_in_A1_._k_)_)_)
percases ( n = 0 or ex n1 being Nat st n = n1 + 1 ) by NAT_1:6;
case n = 0 ; ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) )
hence ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) by A1, Def3, NAT_1:2; ::_thesis: verum
end;
case ex n1 being Nat st n = n1 + 1 ; ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) )
then consider n1 being Nat such that
A2: n = n1 + 1 ;
A3: x in (A1 . (n1 + 1)) \ ((Partial_Union A1) . n1) by A1, A2, Def3;
then A4: not x in (Partial_Union A1) . n1 by XBOOLE_0:def_5;
for k being Nat st k < n holds
not x in A1 . k
proof
let k be Nat; ::_thesis: ( k < n implies not x in A1 . k )
assume k < n ; ::_thesis: not x in A1 . k
then k <= n1 by A2, NAT_1:13;
hence not x in A1 . k by A4, Th13; ::_thesis: verum
end;
hence ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) by A2, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) ; ::_thesis: verum
end;
assume that
A5: x in A1 . n and
A6: for k being Nat st k < n holds
not x in A1 . k ; ::_thesis: x in (Partial_Diff_Union A1) . n
now__::_thesis:_(_(_n_=_0_&_x_in_(Partial_Diff_Union_A1)_._n_)_or_(_ex_n1_being_Nat_st_n_=_n1_+_1_&_x_in_(Partial_Diff_Union_A1)_._n_)_)
percases ( n = 0 or ex n1 being Nat st n = n1 + 1 ) by NAT_1:6;
case n = 0 ; ::_thesis: x in (Partial_Diff_Union A1) . n
hence x in (Partial_Diff_Union A1) . n by A5, Def3; ::_thesis: verum
end;
case ex n1 being Nat st n = n1 + 1 ; ::_thesis: x in (Partial_Diff_Union A1) . n
then consider n1 being Nat such that
A7: n = n1 + 1 ;
for k being Nat st k <= n1 holds
not x in A1 . k
proof
let k be Nat; ::_thesis: ( k <= n1 implies not x in A1 . k )
assume k <= n1 ; ::_thesis: not x in A1 . k
then k < n1 + 1 by NAT_1:13;
hence not x in A1 . k by A6, A7; ::_thesis: verum
end;
then not x in (Partial_Union A1) . n1 by Th13;
then x in (A1 . (n1 + 1)) \ ((Partial_Union A1) . n1) by A5, A7, XBOOLE_0:def_5;
hence x in (Partial_Diff_Union A1) . n by A7, Def3; ::_thesis: verum
end;
end;
end;
hence x in (Partial_Diff_Union A1) . n ; ::_thesis: verum
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
let n be Nat; ::_thesis: for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n
let X be set ; ::_thesis: for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n
let A1 be SetSequence of X; ::_thesis: (Partial_Diff_Union A1) . n c= A1 . n
for x being set st x in (Partial_Diff_Union A1) . n holds
x in A1 . n by Th16;
hence (Partial_Diff_Union A1) . n c= A1 . n by TARSKI:def_3; ::_thesis: verum
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
let n be Nat; ::_thesis: for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
let X be set ; ::_thesis: for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
let A1 be SetSequence of X; ::_thesis: (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
( (Partial_Diff_Union A1) . n c= A1 . n & A1 . n c= (Partial_Union A1) . n ) by Th9, Th17;
hence (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n by XBOOLE_1:1; ::_thesis: verum
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
let X be set ; ::_thesis: for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
let A1 be SetSequence of X; ::_thesis: Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
for n being Element of NAT holds (Partial_Union (Partial_Diff_Union A1)) . n = (Partial_Union A1) . n
proof
set A2 = Partial_Diff_Union A1;
defpred S1[ set ] means (Partial_Union (Partial_Diff_Union A1)) . $1 = (Partial_Union A1) . $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: (Partial_Union (Partial_Diff_Union A1)) . k = (Partial_Union A1) . k ; ::_thesis: S1[k + 1]
thus (Partial_Union (Partial_Diff_Union A1)) . (k + 1) = ((Partial_Diff_Union A1) . (k + 1)) \/ ((Partial_Union (Partial_Diff_Union A1)) . k) by Def2
.= ((A1 . (k + 1)) \ ((Partial_Union A1) . k)) \/ ((Partial_Union A1) . k) by A2, Def3
.= (A1 . (k + 1)) \/ ((Partial_Union A1) . k) by XBOOLE_1:39
.= (Partial_Union A1) . (k + 1) by Def2 ; ::_thesis: verum
end;
(Partial_Union (Partial_Diff_Union A1)) . 0 = (Partial_Diff_Union A1) . 0 by Def2
.= A1 . 0 by Def3
.= (Partial_Union A1) . 0 by Def2 ;
then A3: S1[ 0 ] ;
thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;
hence Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 by FUNCT_2:63; ::_thesis: verum
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
let X be set ; ::_thesis: for A1 being SetSequence of X holds Union (Partial_Diff_Union A1) = Union A1
let A1 be SetSequence of X; ::_thesis: Union (Partial_Diff_Union A1) = Union A1
thus Union (Partial_Diff_Union A1) = Union (Partial_Union (Partial_Diff_Union A1)) by Th15
.= Union (Partial_Union A1) by Th19
.= Union A1 by Th15 ; ::_thesis: verum
end;
definition
let X be set ;
let A1 be SetSequence of X;
:: original: disjoint_valued
redefine attrA1 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
thus ( A1 is V73() implies for m, n being Nat st m <> n holds
A1 . m misses A1 . n ) by PROB_2:def_2; ::_thesis: ( ( for m, n being Nat st m <> n holds
A1 . m misses A1 . n ) implies A1 is disjoint_valued )
assume A1: for m, n being Nat st m <> n holds
A1 . m misses A1 . n ; ::_thesis: A1 is disjoint_valued
now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_
A1_._x_misses_A1_._y
let x, y be set ; ::_thesis: ( x <> y implies A1 . b1 misses A1 . b2 )
assume A2: x <> y ; ::_thesis: A1 . b1 misses A1 . b2
percases ( ( x in dom A1 & y in dom A1 ) or not x in dom A1 or not y in dom A1 ) ;
suppose ( x in dom A1 & y in dom A1 ) ; ::_thesis: A1 . b1 misses A1 . b2
hence A1 . x misses A1 . y by A1, A2; ::_thesis: verum
end;
suppose ( not x in dom A1 or not y in dom A1 ) ; ::_thesis: A1 . b1 misses A1 . b2
then ( A1 . x = {} or A1 . y = {} ) by FUNCT_1:def_2;
hence A1 . x misses A1 . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence A1 is disjoint_valued by PROB_2:def_2; ::_thesis: verum
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
for m, n being Nat st m <> n holds
(Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m
proof
let m, n be Nat; ::_thesis: ( m <> n implies (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m )
assume A1: m <> n ; ::_thesis: (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m
assume (Partial_Diff_Union A1) . n meets (Partial_Diff_Union A1) . m ; ::_thesis: contradiction
then consider x being set such that
A2: x in (Partial_Diff_Union A1) . n and
A3: x in (Partial_Diff_Union A1) . m by XBOOLE_0:3;
percases ( m < n or n < m ) by A1, XXREAL_0:1;
suppose m < n ; ::_thesis: contradiction
then not x in A1 . m by A2, Th16;
hence contradiction by A3, Th16; ::_thesis: verum
end;
suppose n < m ; ::_thesis: contradiction
then not x in A1 . n by A3, Th16;
hence contradiction by A2, Th16; ::_thesis: verum
end;
end;
end;
hence Partial_Diff_Union A1 is disjoint_valued by Def4; ::_thesis: verum
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
defpred S1[ set ] means (Partial_Intersection XSeq) . X in Si;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: (Partial_Intersection XSeq) . k in Si ; ::_thesis: S1[k + 1]
((Partial_Intersection XSeq) . k) /\ (XSeq . (k + 1)) is Event of Si by A2, PROB_1:19;
then ((Partial_Intersection XSeq) . k) /\ (XSeq . (k + 1)) in Si ;
hence S1[k + 1] by Def1; ::_thesis: verum
end;
( XSeq . 0 in rng XSeq & (Partial_Intersection XSeq) . 0 = XSeq . 0 ) by Def1, NAT_1:51;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
then rng (Partial_Intersection XSeq) c= Si by NAT_1:52;
hence Partial_Intersection XSeq is Si -valued by RELAT_1:def_19; ::_thesis: verum
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
defpred S1[ set ] means (Partial_Union XSeq) . X in Si;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: (Partial_Union XSeq) . k in Si ; ::_thesis: S1[k + 1]
((Partial_Union XSeq) . k) \/ (XSeq . (k + 1)) is Event of Si by A2, PROB_1:21;
then ((Partial_Union XSeq) . k) \/ (XSeq . (k + 1)) in Si ;
hence S1[k + 1] by Def2; ::_thesis: verum
end;
( XSeq . 0 in rng XSeq & (Partial_Union XSeq) . 0 = XSeq . 0 ) by Def2, NAT_1:51;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
then rng (Partial_Union XSeq) c= Si by NAT_1:52;
hence Partial_Union XSeq is Si -valued by RELAT_1:def_19; ::_thesis: verum
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
A1: ( XSeq . 0 in rng XSeq & (Partial_Diff_Union XSeq) . 0 = XSeq . 0 ) by Def3, NAT_1:51;
for m being Nat holds (Partial_Diff_Union XSeq) . m in Si
proof
let m be Nat; ::_thesis: (Partial_Diff_Union XSeq) . m in Si
now__::_thesis:_(_(_m_=_0_&_(Partial_Diff_Union_XSeq)_._m_in_Si_)_or_(_ex_k_being_Nat_st_m_=_k_+_1_&_(Partial_Diff_Union_XSeq)_._m_in_Si_)_)
percases ( m = 0 or ex k being Nat st m = k + 1 ) by NAT_1:6;
case m = 0 ; ::_thesis: (Partial_Diff_Union XSeq) . m in Si
hence (Partial_Diff_Union XSeq) . m in Si by A1; ::_thesis: verum
end;
case ex k being Nat st m = k + 1 ; ::_thesis: (Partial_Diff_Union XSeq) . m in Si
then consider k being Nat such that
A2: m = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(XSeq . (k + 1)) \ ((Partial_Union XSeq) . k) in Si ;
hence (Partial_Diff_Union XSeq) . m in Si by A2, Def3; ::_thesis: verum
end;
end;
end;
hence (Partial_Diff_Union XSeq) . m in Si ; ::_thesis: verum
end;
then rng (Partial_Diff_Union XSeq) c= Si by NAT_1:52;
hence Partial_Diff_Union XSeq is Si -valued by RELAT_1:def_19; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing
let P be Probability of Sigma; ::_thesis: P * (Partial_Union ASeq) is non-decreasing
Partial_Union ASeq is V71() by Th11;
hence P * (Partial_Union ASeq) is non-decreasing by Th6; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing
let P be Probability of Sigma; ::_thesis: P * (Partial_Intersection ASeq) is non-increasing
Partial_Intersection ASeq is V70() by Th10;
hence P * (Partial_Intersection ASeq) is non-increasing by Th7; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing
let P be Probability of Sigma; ::_thesis: Partial_Sums (P * ASeq) is non-decreasing
for n being Element of NAT holds (P * ASeq) . n >= 0 by Th4;
hence Partial_Sums (P * ASeq) is non-decreasing by SERIES_1:16; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0
let P be Probability of Sigma; ::_thesis: (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0
A1: dom (P * ASeq) = NAT by SEQ_1:1;
dom (P * (Partial_Union ASeq)) = NAT by SEQ_1:1;
then A2: (P * (Partial_Union ASeq)) . 0 = P . ((Partial_Union ASeq) . 0) by FUNCT_1:12
.= P . (ASeq . 0) by Def2 ;
(Partial_Sums (P * ASeq)) . 0 = (P * ASeq) . 0 by SERIES_1:def_1
.= P . (ASeq . 0) by A1, FUNCT_1:12 ;
hence (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 by A2; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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) )
let Sigma be SigmaField of Omega; ::_thesis: 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) )
let ASeq be SetSequence of Sigma; ::_thesis: 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) )
let P be Probability of Sigma; ::_thesis: ( 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) )
A1: P * (Partial_Union ASeq) is non-decreasing by Th37;
A2: Partial_Union ASeq is V71() by Th11;
then P * (Partial_Union ASeq) is convergent by PROB_2:10;
then A3: P * (Partial_Union ASeq) is bounded ;
lim (P * (Partial_Union ASeq)) = P . (Union (Partial_Union ASeq)) by A2, PROB_2:10
.= P . (Union ASeq) by Th15 ;
hence ( 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) ) by A2, A3, A1, PROB_2:10, RINFSUP1:24; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: 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
let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is V73() implies for n, m being Nat st n < m holds
(Partial_Union ASeq) . n misses ASeq . m )
assume A1: ASeq is V73() ; ::_thesis: for n, m being Nat st n < m holds
(Partial_Union ASeq) . n misses ASeq . m
let n, m be Nat; ::_thesis: ( n < m implies (Partial_Union ASeq) . n misses ASeq . m )
assume A2: n < m ; ::_thesis: (Partial_Union ASeq) . n misses ASeq . m
assume (Partial_Union ASeq) . n meets ASeq . m ; ::_thesis: contradiction
then consider x being set such that
A3: x in (Partial_Union ASeq) . n and
A4: x in ASeq . m by XBOOLE_0:3;
consider k being Nat such that
A5: k <= n and
A6: x in ASeq . k by A3, Th13;
( m in NAT & k in NAT ) by ORDINAL1:def_12;
then ASeq . k misses ASeq . m by A1, A2, A5, PROB_2:def_3;
then (ASeq . k) /\ (ASeq . m) = {} by XBOOLE_0:def_7;
hence contradiction by A4, A6, XBOOLE_0:def_4; ::_thesis: verum
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
let n be Nat; ::_thesis: 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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: 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
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds
(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n
let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n )
A1: dom (P * ASeq) = NAT by SEQ_1:1;
defpred S1[ Nat] means (P * (Partial_Union ASeq)) . $1 = (Partial_Sums (P * ASeq)) . $1;
A2: dom (P * (Partial_Union ASeq)) = NAT by SEQ_1:1;
assume A3: ASeq is V73() ; ::_thesis: (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: (P * (Partial_Union ASeq)) . k = (Partial_Sums (P * ASeq)) . k ; ::_thesis: S1[k + 1]
k < k + 1 by NAT_1:13;
then A6: (Partial_Union ASeq) . k misses ASeq . (k + 1) by A3, Th42;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A7: (Partial_Sums (P * ASeq)) . (k + 1) = ((Partial_Sums (P * ASeq)) . k) + ((P * ASeq) . (k + 1)) by SERIES_1:def_1
.= ((Partial_Sums (P * ASeq)) . k) + (P . (ASeq . (k + 1))) by A1, FUNCT_1:12 ;
(P * (Partial_Union ASeq)) . (k + 1) = P . ((Partial_Union ASeq) . (k + 1)) by A2, FUNCT_1:12
.= P . (((Partial_Union ASeq) . k) \/ (ASeq . (k + 1))) by Def2
.= (P . ((Partial_Union ASeq) . k)) + (P . (ASeq . (k + 1))) by A6, PROB_1:def_8
.= ((P * (Partial_Union ASeq)) . k) + (P . (ASeq . (k + 1))) by A2, FUNCT_1:12 ;
hence S1[k + 1] by A5, A7; ::_thesis: verum
end;
A8: S1[ 0 ] by Th40;
for k being Nat holds S1[k] from NAT_1:sch_2(A8, A4);
hence (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n ; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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)
let Sigma be SigmaField of Omega; ::_thesis: 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)
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds
P * (Partial_Union ASeq) = Partial_Sums (P * ASeq)
let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) )
assume ASeq is V73() ; ::_thesis: P * (Partial_Union ASeq) = Partial_Sums (P * ASeq)
then for n being Element of NAT holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n by Th43;
hence P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by FUNCT_2:63; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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) )
let Sigma be SigmaField of Omega; ::_thesis: 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) )
let ASeq be SetSequence of Sigma; ::_thesis: 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) )
let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies ( 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) ) )
assume ASeq is V73() ; ::_thesis: ( 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) )
then P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th44;
hence ( 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) ) by Th41; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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)
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V73() holds
P . (Union ASeq) = Sum (P * ASeq)
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds
P . (Union ASeq) = Sum (P * ASeq)
let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies P . (Union ASeq) = Sum (P * ASeq) )
assume ASeq is V73() ; ::_thesis: P . (Union ASeq) = Sum (P * ASeq)
then lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) by Th45;
hence P . (Union ASeq) = Sum (P * ASeq) by SERIES_1:def_3; ::_thesis: verum
end;
definition
let X be set ;
let F1 be FinSequence of bool X;
let n be Nat;
:: original: .
redefine funcF1 . n -> Subset of X;
coherence
F1 . n is Subset of X
proof
percases ( n in dom F1 or not n in dom F1 ) ;
suppose n in dom F1 ; ::_thesis: F1 . n is Subset of X
hence F1 . n is Subset of X by FINSEQ_2:11; ::_thesis: verum
end;
suppose not n in dom F1 ; ::_thesis: F1 . n is Subset of X
then F1 . n = {} by FUNCT_1:def_2;
hence F1 . n is Subset of X by SUBSET_1:1; ::_thesis: verum
end;
end;
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
let X be set ; ::_thesis: ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X
now__::_thesis:_for_n_being_Element_of_NAT_ex_F1_being_FinSequence_of_bool_X_st_
for_k_being_Nat_st_k_in_dom_F1_holds_
F1_._k_=_X
let n be Element of NAT ; ::_thesis: ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X
set F1 = n |-> X;
A1: dom (n |-> X) = Seg n by FUNCOP_1:13;
rng (n |-> X) c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (n |-> X) or x in bool X )
assume x in rng (n |-> X) ; ::_thesis: x in bool X
then ex i being Nat st
( i in dom (n |-> X) & (n |-> X) . i = x ) by FINSEQ_2:10;
then x = X by A1, FINSEQ_2:57;
hence x in bool X by ZFMISC_1:def_1; ::_thesis: verum
end;
then A2: n |-> X is FinSequence of bool X by FINSEQ_1:def_4;
for k being Nat st k in dom (n |-> X) holds
(n |-> X) . k = X by A1, FINSEQ_2:57;
hence ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X by A2; ::_thesis: verum
end;
hence ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X ; ::_thesis: verum
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
Union F1 = union (rng F1) by CARD_3:def_4;
hence Union F1 is Subset of X ; ::_thesis: verum
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
let X, x be set ; ::_thesis: 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 ) )
let F1 be FinSequence of bool X; ::_thesis: ( x in Union F1 iff ex k being Nat st
( k in dom F1 & x in F1 . k ) )
set Y = union (rng F1);
A1: for x being set holds
( x in union (rng F1) iff ex k being Nat st
( k in dom F1 & x in F1 . k ) )
proof
let x be set ; ::_thesis: ( x in union (rng F1) iff ex k being Nat st
( k in dom F1 & x in F1 . k ) )
thus ( x in union (rng F1) implies ex k being Nat st
( k in dom F1 & x in F1 . k ) ) ::_thesis: ( ex k being Nat st
( k in dom F1 & x in F1 . k ) implies x in union (rng F1) )
proof
assume x in union (rng F1) ; ::_thesis: ex k being Nat st
( k in dom F1 & x in F1 . k )
then consider Z being set such that
A2: x in Z and
A3: Z in rng F1 by TARSKI:def_4;
ex i being Nat st
( i in dom F1 & Z = F1 . i ) by A3, FINSEQ_2:10;
hence ex k being Nat st
( k in dom F1 & x in F1 . k ) by A2; ::_thesis: verum
end;
thus ( ex k being Nat st
( k in dom F1 & x in F1 . k ) implies x in union (rng F1) ) ::_thesis: verum
proof
given i being Nat such that A4: i in dom F1 and
A5: x in F1 . i ; ::_thesis: x in union (rng F1)
F1 . i in rng F1 by A4, FUNCT_1:def_3;
hence x in union (rng F1) by A5, TARSKI:def_4; ::_thesis: verum
end;
end;
union (rng F1) = Union F1 by CARD_3:def_4;
hence ( x in Union F1 iff ex k being Nat st
( k in dom F1 & x in F1 . k ) ) by A1; ::_thesis: verum
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
deffunc H1( Nat) -> Element of K10(X) = (F1 . $1) ` ;
consider f being FinSequence of bool X such that
A1: ( len f = len F1 & ( for n being Nat st n in dom f holds
f . n = H1(n) ) ) from FINSEQ_2:sch_1();
take f ; ::_thesis: ( len f = len F1 & ( for n being Nat st n in dom f holds
f . n = (F1 . n) ` ) )
thus ( len f = len F1 & ( for n being Nat st n in dom f holds
f . n = (F1 . n) ` ) ) by A1; ::_thesis: verum
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
let F2, F3 be FinSequence of bool X; ::_thesis: ( len F2 = len F1 & ( for n being Nat st n in dom F2 holds
F2 . n = (F1 . n) ` ) & len F3 = len F1 & ( for n being Nat st n in dom F3 holds
F3 . n = (F1 . n) ` ) implies F2 = F3 )
assume that
A2: len F2 = len F1 and
A3: for n being Nat st n in dom F2 holds
F2 . n = (F1 . n) ` and
A4: len F3 = len F1 and
A5: for n being Nat st n in dom F3 holds
F3 . n = (F1 . n) ` ; ::_thesis: F2 = F3
( dom F2 = dom F3 & ( for k being Nat st k in dom F2 holds
F2 . k = F3 . k ) )
proof
thus A6: dom F2 = Seg (len F3) by A2, A4, FINSEQ_1:def_3
.= dom F3 by FINSEQ_1:def_3 ; ::_thesis: for k being Nat st k in dom F2 holds
F2 . k = F3 . k
let k be Nat; ::_thesis: ( k in dom F2 implies F2 . k = F3 . k )
assume A7: k in dom F2 ; ::_thesis: F2 . k = F3 . k
hence F2 . k = (F1 . k) ` by A3
.= F3 . k by A5, A6, A7 ;
::_thesis: verum
end;
hence F2 = F3 by FINSEQ_1:13; ::_thesis: verum
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
let X be set ; ::_thesis: for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1
let F1 be FinSequence of bool X; ::_thesis: dom (Complement F1) = dom F1
thus dom (Complement F1) = Seg (len (Complement F1)) by FINSEQ_1:def_3
.= Seg (len F1) by Def5
.= dom F1 by FINSEQ_1:def_3 ; ::_thesis: verum
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
let X, x be set ; ::_thesis: 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 )
let F1 be FinSequence of bool X; ::_thesis: ( F1 <> {} implies ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k ) )
A1: for n being Nat st n in dom F1 holds
X \ ((Complement F1) . n) = F1 . n
proof
let n be Nat; ::_thesis: ( n in dom F1 implies X \ ((Complement F1) . n) = F1 . n )
assume n in dom F1 ; ::_thesis: X \ ((Complement F1) . n) = F1 . n
then A2: n in dom (Complement F1) by Th50;
X \ ((Complement F1) . n) = ((Complement F1) . n) ` by SUBSET_1:def_4
.= ((F1 . n) `) ` by A2, Def5
.= F1 . n ;
hence X \ ((Complement F1) . n) = F1 . n ; ::_thesis: verum
end;
assume A3: F1 <> {} ; ::_thesis: ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )
then A4: dom F1 <> {} by RELAT_1:41;
A5: ( ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) iff for n being Nat st n in dom F1 holds
x in F1 . n )
proof
hereby ::_thesis: ( ( for n being Nat st n in dom F1 holds
x in F1 . n ) implies ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) )
assume that
A6: x in X and
A7: for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ; ::_thesis: for n being Nat st n in dom F1 holds
x in F1 . n
let n be Nat; ::_thesis: ( n in dom F1 implies x in F1 . n )
assume A8: n in dom F1 ; ::_thesis: x in F1 . n
not x in (Complement F1) . n by A7, A8;
then x in X \ ((Complement F1) . n) by A6, XBOOLE_0:def_5;
hence x in F1 . n by A1, A8; ::_thesis: verum
end;
assume A9: for n being Nat st n in dom F1 holds
x in F1 . n ; ::_thesis: ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) )
A10: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F1_holds_
(_x_in_X_&_not_x_in_(Complement_F1)_._n_)
let n be Element of NAT ; ::_thesis: ( n in dom F1 implies ( x in X & not x in (Complement F1) . n ) )
assume A11: n in dom F1 ; ::_thesis: ( x in X & not x in (Complement F1) . n )
x in F1 . n by A9, A11;
then x in X \ ((Complement F1) . n) by A1, A11;
hence ( x in X & not x in (Complement F1) . n ) by XBOOLE_0:def_5; ::_thesis: verum
end;
ex a being set st a in dom F1 by A4, XBOOLE_0:def_1;
hence ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) by A10; ::_thesis: verum
end;
dom (Complement F1) = dom F1 by Th50;
then A12: ( x in X & not x in Union (Complement F1) iff ( x in X & ( for n being Nat st n in dom F1 holds
not x in (Complement F1) . n ) ) ) by Th49;
( x in (Union (Complement F1)) ` iff x in X \ (Union (Complement F1)) ) by SUBSET_1:def_4;
hence ( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k ) by A3, A12, A5, Def6, XBOOLE_0:def_5; ::_thesis: verum
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
let X, x be set ; ::_thesis: 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 )
let F1 be FinSequence of bool X; ::_thesis: ( F1 <> {} implies ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n ) )
assume F1 <> {} ; ::_thesis: ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n )
then A1: rng F1 <> {} by RELAT_1:41;
A2: now__::_thesis:_for_x_being_set_st_(_for_n_being_Nat_st_n_in_dom_F1_holds_
x_in_F1_._n_)_holds_
x_in_meet_(rng_F1)
let x be set ; ::_thesis: ( ( for n being Nat st n in dom F1 holds
x in F1 . n ) implies x in meet (rng F1) )
assume A3: for n being Nat st n in dom F1 holds
x in F1 . n ; ::_thesis: x in meet (rng F1)
now__::_thesis:_for_Y_being_set_st_Y_in_rng_F1_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in rng F1 implies x in Y )
assume Y in rng F1 ; ::_thesis: x in Y
then consider n being set such that
A4: n in dom F1 and
A5: Y = F1 . n by FUNCT_1:def_3;
thus x in Y by A3, A4, A5; ::_thesis: verum
end;
hence x in meet (rng F1) by A1, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F1)_holds_
for_n_being_Nat_st_n_in_dom_F1_holds_
x_in_F1_._n
let x be set ; ::_thesis: ( x in meet (rng F1) implies for n being Nat st n in dom F1 holds
x in F1 . n )
assume A6: x in meet (rng F1) ; ::_thesis: for n being Nat st n in dom F1 holds
x in F1 . n
now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_
x_in_F1_._k
let k be Nat; ::_thesis: ( k in dom F1 implies x in F1 . k )
assume k in dom F1 ; ::_thesis: x in F1 . k
then F1 . k in rng F1 by FUNCT_1:3;
hence x in F1 . k by A6, SETFAM_1:def_1; ::_thesis: verum
end;
hence for n being Nat st n in dom F1 holds
x in F1 . n ; ::_thesis: verum
end;
hence ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n ) by A2; ::_thesis: verum
end;
theorem :: PROB_3:53
for X being set
for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)
proof
let X be set ; ::_thesis: for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)
let F1 be FinSequence of bool X; ::_thesis: Intersection F1 = meet (rng F1)
percases ( F1 <> {} or F1 = {} ) ;
supposeA1: F1 <> {} ; ::_thesis: Intersection F1 = meet (rng F1)
now__::_thesis:_for_x_being_set_holds_
(_x_in_Intersection_F1_iff_x_in_meet_(rng_F1)_)
let x be set ; ::_thesis: ( x in Intersection F1 iff x in meet (rng F1) )
( x in Intersection F1 iff for n being Nat st n in dom F1 holds
x in F1 . n ) by A1, Th51;
hence ( x in Intersection F1 iff x in meet (rng F1) ) by A1, Th52; ::_thesis: verum
end;
hence Intersection F1 = meet (rng F1) by TARSKI:1; ::_thesis: verum
end;
suppose F1 = {} ; ::_thesis: Intersection F1 = meet (rng F1)
hence Intersection F1 = meet (rng F1) by Def6, RELAT_1:38, SETFAM_1:1; ::_thesis: verum
end;
end;
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
let X be set ; ::_thesis: 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 = {} ) )
deffunc H1( set ) -> set = {} ;
let F1 be FinSequence of bool X; ::_thesis: 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 = {} ) )
defpred S1[ set ] means $1 in dom F1;
deffunc H2( set ) -> set = F1 . $1;
ex f being Function st
( dom f = NAT & ( for k being set st k in NAT holds
( ( S1[k] implies f . k = H2(k) ) & ( not S1[k] implies f . k = H1(k) ) ) ) ) from PARTFUN1:sch_1();
then consider f being Function such that
A1: dom f = NAT and
A2: for x being set st x in NAT holds
( ( x in dom F1 implies f . x = F1 . x ) & ( not x in dom F1 implies f . x = {} ) ) ;
A3: for x being set st x in dom F1 holds
F1 . x in bool X
proof
let x be set ; ::_thesis: ( x in dom F1 implies F1 . x in bool X )
assume x in dom F1 ; ::_thesis: F1 . x in bool X
then F1 . x in rng F1 by FUNCT_1:3;
hence F1 . x in bool X ; ::_thesis: verum
end;
for x being set st x in NAT holds
f . x in bool X
proof
let x be set ; ::_thesis: ( x in NAT implies f . x in bool X )
assume A4: x in NAT ; ::_thesis: f . x in bool X
percases ( not x in dom F1 or x in dom F1 ) ;
suppose not x in dom F1 ; ::_thesis: f . x in bool X
then f . x = {} by A2, A4;
then f . x c= X by XBOOLE_1:2;
hence f . x in bool X ; ::_thesis: verum
end;
supposeA5: x in dom F1 ; ::_thesis: f . x in bool X
then f . x = F1 . x by A2;
hence f . x in bool X by A3, A5; ::_thesis: verum
end;
end;
end;
then reconsider f = f as SetSequence of X by A1, FUNCT_2:3;
take f ; ::_thesis: ( ( for k being Nat st k in dom F1 holds
f . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
f . k = {} ) )
thus for k being Nat st k in dom F1 holds
f . k = F1 . k by A2; ::_thesis: for k being Nat st not k in dom F1 holds
f . k = {}
let k be Nat; ::_thesis: ( not k in dom F1 implies f . k = {} )
k in NAT by ORDINAL1:def_12;
hence ( not k in dom F1 implies f . k = {} ) by A2; ::_thesis: verum
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
let X be set ; ::_thesis: 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 )
let F1 be FinSequence of bool X; ::_thesis: 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 )
let A1 be SetSequence of X; ::_thesis: ( ( 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 = {} ) implies ( A1 . 0 = {} & Union A1 = Union F1 ) )
assume that
A1: for k being Nat st k in dom F1 holds
A1 . k = F1 . k and
A2: for k being Nat st not k in dom F1 holds
A1 . k = {} ; ::_thesis: ( A1 . 0 = {} & Union A1 = Union F1 )
thus A1 . 0 = {} by A2, Th1; ::_thesis: Union A1 = Union F1
thus Union A1 = Union F1 ::_thesis: verum
proof
thus Union A1 c= Union F1 :: according to XBOOLE_0:def_10 ::_thesis: Union F1 c= Union A1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union A1 or x in Union F1 )
assume x in Union A1 ; ::_thesis: x in Union F1
then consider n being Element of NAT such that
A3: x in A1 . n by PROB_1:12;
( n in dom F1 & x in F1 . n ) by A1, A2, A3;
hence x in Union F1 by Th49; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union F1 or x in Union A1 )
assume x in Union F1 ; ::_thesis: x in Union A1
then consider n being Nat such that
A4: ( n in dom F1 & x in F1 . n ) by Th49;
( n in NAT & x in A1 . n ) by A1, A4;
hence x in Union A1 by PROB_1:12; ::_thesis: verum
end;
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
let f be FinSequence of Si; ::_thesis: f is FinSequence of bool X
thus rng f c= bool X by XBOOLE_1:1; :: according to FINSEQ_1:def_4 ::_thesis: verum
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 funcFSi . n -> Event of Si;
coherence
FSi . n is Event of Si
proof
percases ( n in dom FSi or not n in dom FSi ) ;
suppose n in dom FSi ; ::_thesis: FSi . n is Event of Si
hence FSi . n is Event of Si by FINSEQ_2:11; ::_thesis: verum
end;
suppose not n in dom FSi ; ::_thesis: FSi . n is Event of Si
then FSi . n = {} by FUNCT_1:def_2;
hence FSi . n is Event of Si by PROB_1:22; ::_thesis: verum
end;
end;
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
let X be set ; ::_thesis: 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 = {} ) )
let Si be SigmaField of X; ::_thesis: 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 = {} ) )
let FSi be FinSequence of Si; ::_thesis: 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 = {} ) )
consider A1 being SetSequence of X such that
A1: for k being Nat st k in dom FSi holds
A1 . k = FSi . k and
A2: for k being Nat st not k in dom FSi holds
A1 . k = {} by Th54;
for n being Nat holds A1 . n in Si
proof
let n be Nat; ::_thesis: A1 . n in Si
percases ( not n in dom FSi or n in dom FSi ) ;
suppose not n in dom FSi ; ::_thesis: A1 . n in Si
then A1 . n = {} by A2;
hence A1 . n in Si by PROB_1:4; ::_thesis: verum
end;
suppose n in dom FSi ; ::_thesis: A1 . n in Si
then A1 . n = FSi . n by A1;
hence A1 . n in Si ; ::_thesis: verum
end;
end;
end;
then rng A1 c= Si by NAT_1:52;
then reconsider A1 = A1 as SetSequence of Si by RELAT_1:def_19;
take A1 ; ::_thesis: ( ( for k being Nat st k in dom FSi holds
A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds
A1 . k = {} ) )
thus ( ( for k being Nat st k in dom FSi holds
A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds
A1 . k = {} ) ) by A1, A2; ::_thesis: verum
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
let X be set ; ::_thesis: for Si being SigmaField of X
for FSi being FinSequence of Si holds Union FSi in Si
let Si be SigmaField of X; ::_thesis: for FSi being FinSequence of Si holds Union FSi in Si
let FSi be FinSequence of Si; ::_thesis: Union FSi in Si
consider ASeq being SetSequence of Si such that
A1: ( ( 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 = {} ) ) by Th56;
Union ASeq = Union FSi by A1, Th55;
hence Union FSi in Si by PROB_1:17; ::_thesis: verum
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
set G = Complement F;
let x be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not x in rng (Complement F) or x in S )
assume x in rng (Complement F) ; ::_thesis: x in S
then consider y being set such that
A1: y in dom (Complement F) and
A2: x = (Complement F) . y by FUNCT_1:def_3;
reconsider y = y as Nat by A1;
(Complement F) . y = (F . y) ` by A1, Def5;
then (Complement F) . y is Event of S by PROB_1:20;
hence x in S by A2; ::_thesis: verum
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
let X be set ; ::_thesis: for Si being SigmaField of X
for FSi being FinSequence of Si holds Intersection FSi in Si
let Si be SigmaField of X; ::_thesis: for FSi being FinSequence of Si holds Intersection FSi in Si
let FSi be FinSequence of Si; ::_thesis: Intersection FSi in Si
percases ( FSi = {} or FSi <> {} ) ;
suppose FSi = {} ; ::_thesis: Intersection FSi in Si
then Intersection FSi = {} by Def6;
hence Intersection FSi in Si by PROB_1:4; ::_thesis: verum
end;
supposeA1: FSi <> {} ; ::_thesis: Intersection FSi in Si
rng (Complement FSi) c= Si ;
then reconsider C = Complement FSi as FinSequence of Si by FINSEQ_1:def_4;
A2: Union C in Si by Th57;
Intersection FSi = (Union (Complement FSi)) ` by A1, Def6;
hence Intersection FSi in Si by A2, PROB_1:def_1; ::_thesis: verum
end;
end;
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
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq
let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq
let FSeq be FinSequence of Sigma; ::_thesis: dom (P * FSeq) = dom FSeq
for x being set holds
( x in dom (P * FSeq) iff x in dom FSeq )
proof
let x be set ; ::_thesis: ( x in dom (P * FSeq) iff x in dom FSeq )
thus ( x in dom (P * FSeq) implies x in dom FSeq ) by FUNCT_1:11; ::_thesis: ( x in dom FSeq implies x in dom (P * FSeq) )
assume A1: x in dom FSeq ; ::_thesis: x in dom (P * FSeq)
then reconsider k = x as Element of NAT ;
FSeq . k in Sigma ;
then FSeq . k in dom P by FUNCT_2:def_1;
hence x in dom (P * FSeq) by A1, FUNCT_1:11; ::_thesis: verum
end;
hence dom (P * FSeq) = dom FSeq by TARSKI:1; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL
let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL
let FSeq be FinSequence of Sigma; ::_thesis: P * FSeq is FinSequence of REAL
dom (P * FSeq) = dom FSeq by Th59;
then ex n being Nat st dom (P * FSeq) = Seg n by FINSEQ_1:def_2;
then reconsider RSeq = P * FSeq as FinSequence by FINSEQ_1:def_2;
rng (P * FSeq) c= REAL ;
then rng RSeq c= REAL ;
hence P * FSeq is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum
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 funcP * 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
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq
let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq
let FSeq be FinSequence of Sigma; ::_thesis: len (P * FSeq) = len FSeq
dom (P * FSeq) = dom FSeq by Th59;
then Seg (len (P * FSeq)) = dom FSeq by FINSEQ_1:def_3;
hence len (P * FSeq) = len FSeq by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th62: :: PROB_3:62
for RFin being FinSequence of REAL st len RFin = 0 holds
Sum RFin = 0
proof
let RFin be FinSequence of REAL ; ::_thesis: ( len RFin = 0 implies Sum RFin = 0 )
assume A1: len RFin = 0 ; ::_thesis: Sum RFin = 0
A2: addreal is having_a_unity by RVSUM_1:1, SETWISEO:def_2;
thus Sum RFin = addreal $$ RFin by RVSUM_1:def_12
.= 0 by A1, A2, BINOP_2:2, FINSOP_1:def_1 ; ::_thesis: verum
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
let RFin be FinSequence of REAL ; ::_thesis: ( len RFin >= 1 implies 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) ) )
assume len RFin >= 1 ; ::_thesis: 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) )
then consider f being Function of NAT,REAL such that
A1: f . 1 = RFin . 1 and
A2: for n being Element of NAT st 0 <> n & n < len RFin holds
f . (n + 1) = addreal . ((f . n),(RFin . (n + 1))) and
A3: addreal "**" RFin = f . (len RFin) by FINSOP_1:1;
take f ; ::_thesis: ( 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) )
for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1))
proof
let n be Nat; ::_thesis: ( 0 <> n & n < len RFin implies f . (n + 1) = (f . n) + (RFin . (n + 1)) )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
assume that
A4: 0 <> n and
A5: n < len RFin ; ::_thesis: f . (n + 1) = (f . n) + (RFin . (n + 1))
thus f . (n + 1) = addreal . ((f . n1),(RFin . (n1 + 1))) by A2, A4, A5
.= (f . n) + (RFin . (n + 1)) by BINOP_2:def_9 ; ::_thesis: verum
end;
hence ( 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) ) by A1, A3, RVSUM_1:def_12; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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) )
let Sigma be SigmaField of Omega; ::_thesis: 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) )
let P be Probability of Sigma; ::_thesis: 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) )
let FSeq be FinSequence of Sigma; ::_thesis: 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) )
let ASeq be SetSequence of Sigma; ::_thesis: ( ( 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 = {} ) implies ( 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) ) )
assume that
A1: for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k and
A2: for k being Nat st not k in dom FSeq holds
ASeq . k = {} ; ::_thesis: ( 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) )
A3: ASeq . 0 = {} by A1, A2, Th55;
A4: (P * ASeq) . 0 = P . (ASeq . 0) by FUNCT_2:15
.= 0 by A3, VALUED_0:def_19 ;
A5: for k being Nat st k in dom FSeq holds
(P * ASeq) . k = (P * FSeq) . k
proof
let k be Nat; ::_thesis: ( k in dom FSeq implies (P * ASeq) . k = (P * FSeq) . k )
assume A6: k in dom FSeq ; ::_thesis: (P * ASeq) . k = (P * FSeq) . k
k in NAT by ORDINAL1:def_12;
hence (P * ASeq) . k = P . (ASeq . k) by FUNCT_2:15
.= P . (FSeq . k) by A1, A6
.= (P * FSeq) . k by A6, FUNCT_1:13 ;
::_thesis: verum
end;
1 = 0 + 1 ;
then A7: (Partial_Sums (P * ASeq)) . 1 = ((Partial_Sums (P * ASeq)) . 0) + ((P * ASeq) . 1) by SERIES_1:def_1
.= ((P * ASeq) . 0) + ((P * ASeq) . 1) by SERIES_1:def_1
.= (P * ASeq) . 1 by A4 ;
A8: ( len FSeq >= 1 implies ( (Partial_Sums (P * ASeq)) . 1 = (P * FSeq) . 1 & ( for m being Nat st m <> 0 & m < len FSeq holds
(Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) ) ) )
proof
assume len FSeq >= 1 ; ::_thesis: ( (Partial_Sums (P * ASeq)) . 1 = (P * FSeq) . 1 & ( for m being Nat st m <> 0 & m < len FSeq holds
(Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) ) )
then 1 in dom FSeq by Th2;
hence (Partial_Sums (P * ASeq)) . 1 = (P * FSeq) . 1 by A5, A7; ::_thesis: for m being Nat st m <> 0 & m < len FSeq holds
(Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1))
thus for m being Nat st m <> 0 & m < len FSeq holds
(Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) ::_thesis: verum
proof
let m be Nat; ::_thesis: ( m <> 0 & m < len FSeq implies (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) )
assume that
m <> 0 and
A9: m < len FSeq ; ::_thesis: (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1))
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
m + 1 in Seg (len FSeq) by A9, FINSEQ_3:11;
then A10: m + 1 in dom FSeq by FINSEQ_1:def_3;
thus (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m1) + ((P * ASeq) . (m1 + 1)) by SERIES_1:def_1
.= ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) by A5, A10 ; ::_thesis: verum
end;
end;
defpred S1[ Nat] means (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + $1) = (Partial_Sums (P * ASeq)) . (len FSeq);
A11: for m being Nat holds (P * ASeq) . (((len FSeq) + 1) + m) = 0
proof
set k = (len FSeq) + 1;
let m be Nat; ::_thesis: (P * ASeq) . (((len FSeq) + 1) + m) = 0
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
((len FSeq) + 1) + m >= (len FSeq) + 1 by NAT_1:11;
then ((len FSeq) + 1) + m > len FSeq by Lm1;
then not ((len FSeq) + 1) + m in dom FSeq by FINSEQ_3:25;
then A12: ASeq . (((len FSeq) + 1) + m) = {} by A2;
thus (P * ASeq) . (((len FSeq) + 1) + m) = P . (ASeq . (((len FSeq) + 1) + m1)) by FUNCT_2:15
.= 0 by A12, VALUED_0:def_19 ; ::_thesis: verum
end;
A13: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A14: (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k) = (Partial_Sums (P * ASeq)) . (len FSeq) ; ::_thesis: S1[k + 1]
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
(Partial_Sums (P * ASeq)) . ((((len FSeq) + 1) + k) + 1) = ((Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k1)) + ((P * ASeq) . (((len FSeq) + 1) + (k1 + 1))) by SERIES_1:def_1
.= ((Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k)) + 0 by A11 ;
hence S1[k + 1] by A14; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_(Partial_Diff_Union_ASeq))_._n_<=_(P_*_ASeq)_._n
let n be Element of NAT ; ::_thesis: (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n
(Partial_Diff_Union ASeq) . n c= ASeq . n by Th17;
hence (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by Th5; ::_thesis: verum
end;
then A15: for n being Element of NAT holds (Partial_Sums (P * (Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n by SERIES_1:14;
A16: Partial_Sums (P * (Partial_Diff_Union ASeq)) is convergent by Th45;
(Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + 0) = ((Partial_Sums (P * ASeq)) . (len FSeq)) + ((P * ASeq) . (((len FSeq) + 1) + 0)) by SERIES_1:def_1
.= ((Partial_Sums (P * ASeq)) . (len FSeq)) + 0 by A11 ;
then A17: S1[ 0 ] ;
A18: for k being Nat holds S1[k] from NAT_1:sch_2(A17, A13);
A19: for m being Nat st (len FSeq) + 1 <= m holds
(Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq)
proof
let m be Nat; ::_thesis: ( (len FSeq) + 1 <= m implies (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) )
assume (len FSeq) + 1 <= m ; ::_thesis: (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq)
then ex k being Nat st m = ((len FSeq) + 1) + k by NAT_1:10;
hence (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) by A18; ::_thesis: verum
end;
then A20: lim (Partial_Sums (P * ASeq)) = (Partial_Sums (P * ASeq)) . (len FSeq) by Th3;
then A21: Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) by SERIES_1:def_3;
A22: Sum (P * FSeq) = Sum (P * ASeq)
proof
now__::_thesis:_Sum_(P_*_FSeq)_=_Sum_(P_*_ASeq)
percases ( len FSeq = 0 or len FSeq <> 0 ) ;
suppose len FSeq = 0 ; ::_thesis: Sum (P * FSeq) = Sum (P * ASeq)
then ( len (P * FSeq) = 0 & Sum (P * ASeq) = 0 ) by A4, A21, Th61, SERIES_1:def_1;
hence Sum (P * FSeq) = Sum (P * ASeq) by Th62; ::_thesis: verum
end;
supposeA23: len FSeq <> 0 ; ::_thesis: Sum (P * FSeq) = Sum (P * ASeq)
then 1 <= len FSeq by NAT_1:14;
then A24: 1 <= len (P * FSeq) by Th61;
then consider seq1 being Real_Sequence such that
A25: seq1 . 1 = (P * FSeq) . 1 and
A26: for n being Nat st 0 <> n & n < len (P * FSeq) holds
seq1 . (n + 1) = (seq1 . n) + ((P * FSeq) . (n + 1)) and
A27: Sum (P * FSeq) = seq1 . (len (P * FSeq)) by Th63;
defpred S2[ set , set ] means ex n being Nat st
( n = $1 & ( n = 0 implies $2 = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies $2 = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies $2 = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) );
ex seq being Real_Sequence st
for n being Nat holds
( ( n = 0 implies seq . n = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies seq . n = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies seq . n = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) )
proof
A28: for x being set st x in NAT holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S2[x,y] )
assume x in NAT ; ::_thesis: ex y being set st S2[x,y]
then reconsider n = x as Element of NAT ;
now__::_thesis:_(_(_n_=_0_&_S2[x,_0_]_)_or_(_n_<>_0_&_n_<=_len_(P_*_FSeq)_&_S2[x,seq1_._n]_)_or_(_n_<>_0_&_not_n_<=_len_(P_*_FSeq)_&_S2[x,(Partial_Sums_(P_*_ASeq))_._(len_(P_*_FSeq))]_)_)
percases ( n = 0 or ( n <> 0 & n <= len (P * FSeq) ) or ( n <> 0 & not n <= len (P * FSeq) ) ) ;
case n = 0 ; ::_thesis: S2[x, 0 ]
hence S2[x, 0 ] ; ::_thesis: verum
end;
case ( n <> 0 & n <= len (P * FSeq) ) ; ::_thesis: S2[x,seq1 . n]
hence S2[x,seq1 . n] ; ::_thesis: verum
end;
case ( n <> 0 & not n <= len (P * FSeq) ) ; ::_thesis: S2[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))]
hence S2[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))] ; ::_thesis: verum
end;
end;
end;
hence ex y being set st S2[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A29: ( dom f = NAT & ( for x being set st x in NAT holds
S2[x,f . x] ) ) from CLASSES1:sch_1(A28);
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
f_._x_is_real
let x be set ; ::_thesis: ( x in NAT implies f . x is real )
assume x in NAT ; ::_thesis: f . x is real
then ex n being Nat st
( n = x & ( n = 0 implies f . x = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies f . x = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies f . x = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) ) by A29;
hence f . x is real ; ::_thesis: verum
end;
then reconsider f = f as Real_Sequence by A29, SEQ_1:1;
take seq = f; ::_thesis: for n being Nat holds
( ( n = 0 implies seq . n = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies seq . n = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies seq . n = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) )
let n be Nat; ::_thesis: ( ( n = 0 implies seq . n = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies seq . n = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies seq . n = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) )
n in NAT by ORDINAL1:def_12;
then ex k being Nat st
( k = n & ( k = 0 implies seq . n = 0 ) & ( k <> 0 & k <= len (P * FSeq) implies seq . n = seq1 . k ) & ( k <> 0 & k > len (P * FSeq) implies seq . n = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) ) by A29;
hence ( ( n = 0 implies seq . n = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies seq . n = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies seq . n = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) ) ; ::_thesis: verum
end;
then consider seq2 being Real_Sequence such that
A30: for n being Nat holds
( ( n = 0 implies seq2 . n = 0 ) & ( n <> 0 & n <= len (P * FSeq) implies seq2 . n = seq1 . n ) & ( n <> 0 & n > len (P * FSeq) implies seq2 . n = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) ) ) ;
defpred S3[ Nat] means seq2 . $1 = (Partial_Sums (P * ASeq)) . $1;
A31: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; ::_thesis: ( S3[k] implies S3[k + 1] )
assume A32: S3[k] ; ::_thesis: S3[k + 1]
now__::_thesis:_(_(_k_=_0_&_seq2_._1_=_(Partial_Sums_(P_*_ASeq))_._1_)_or_(_k_<>_0_&_k_<=_(len_(P_*_FSeq))_-_1_&_seq2_._(k_+_1)_=_(Partial_Sums_(P_*_ASeq))_._(k_+_1)_)_or_(_k_<>_0_&_not_k_<=_(len_(P_*_FSeq))_-_1_&_seq2_._(k_+_1)_=_(Partial_Sums_(P_*_ASeq))_._(k_+_1)_)_)
percases ( k = 0 or ( k <> 0 & k <= (len (P * FSeq)) - 1 ) or ( k <> 0 & not k <= (len (P * FSeq)) - 1 ) ) ;
case k = 0 ; ::_thesis: seq2 . 1 = (Partial_Sums (P * ASeq)) . 1
thus seq2 . 1 = (Partial_Sums (P * ASeq)) . 1 by A8, A23, A24, A25, A30, NAT_1:14; ::_thesis: verum
end;
caseA33: ( k <> 0 & k <= (len (P * FSeq)) - 1 ) ; ::_thesis: seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (k + 1)
then A34: k + 0 < ((len (P * FSeq)) - 1) + 1 by XREAL_1:8;
then A35: k < len FSeq by Th61;
k + 1 <= ((len (P * FSeq)) - 1) + 1 by A33, XREAL_1:7;
hence seq2 . (k + 1) = seq1 . (k + 1) by A30
.= (seq1 . k) + ((P * FSeq) . (k + 1)) by A26, A33, A34
.= ((Partial_Sums (P * ASeq)) . k) + ((P * FSeq) . (k + 1)) by A30, A32, A33, A34
.= (Partial_Sums (P * ASeq)) . (k + 1) by A8, A23, A33, A35, NAT_1:14 ;
::_thesis: verum
end;
case ( k <> 0 & not k <= (len (P * FSeq)) - 1 ) ; ::_thesis: seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (k + 1)
then A36: k + 1 > ((len (P * FSeq)) - 1) + 1 by XREAL_1:8;
then k + 1 >= (len (P * FSeq)) + 1 by NAT_1:13;
then consider i being Nat such that
A37: k + 1 = ((len (P * FSeq)) + 1) + i by NAT_1:10;
thus seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) by A30, A36
.= (Partial_Sums (P * ASeq)) . (len FSeq) by Th61
.= (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + i) by A18
.= (Partial_Sums (P * ASeq)) . (k + 1) by A37, Th61 ; ::_thesis: verum
end;
end;
end;
hence S3[k + 1] ; ::_thesis: verum
end;
seq2 . 0 = (P * ASeq) . 0 by A4, A30
.= (Partial_Sums (P * ASeq)) . 0 by SERIES_1:def_1 ;
then A38: S3[ 0 ] ;
A39: for k being Nat holds S3[k] from NAT_1:sch_2(A38, A31);
len (P * FSeq) <> 0 by A23, Th61;
then seq2 . (len (P * FSeq)) = Sum (P * FSeq) by A27, A30;
hence Sum (P * FSeq) = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) by A39
.= Sum (P * ASeq) by A21, Th61 ;
::_thesis: verum
end;
end;
end;
hence Sum (P * FSeq) = Sum (P * ASeq) ; ::_thesis: verum
end;
Partial_Sums (P * ASeq) is convergent by A19, Th3;
then lim (Partial_Sums (P * (Partial_Diff_Union ASeq))) <= lim (Partial_Sums (P * ASeq)) by A16, A15, SEQ_2:18;
then Sum (P * (Partial_Diff_Union ASeq)) <= lim (Partial_Sums (P * ASeq)) by SERIES_1:def_3;
then Sum (P * (Partial_Diff_Union ASeq)) <= Sum (P * ASeq) by SERIES_1:def_3;
then P . (Union (Partial_Diff_Union ASeq)) <= Sum (P * ASeq) by Th46;
hence ( 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) ) by A19, A20, A22, Th3, Th20, SERIES_1:def_3; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: 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) ) )
let Sigma be SigmaField of Omega; ::_thesis: 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) ) )
let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
let FSeq be FinSequence of Sigma; ::_thesis: ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
consider ASeq being SetSequence of Sigma such that
A1: for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k and
A2: for k being Nat st not k in dom FSeq holds
ASeq . k = {} by Th56;
P . (Union ASeq) = P . (Union FSeq) by A1, A2, Th55;
then P . (Union FSeq) <= Sum (P * ASeq) by A1, A2, Th64;
hence P . (Union FSeq) <= Sum (P * FSeq) by A1, A2, Th64; ::_thesis: ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) )
assume A3: FSeq is disjoint_valued ; ::_thesis: P . (Union FSeq) = Sum (P * FSeq)
A4: ( FSeq is disjoint_valued implies ASeq is V73() )
proof
assume A5: FSeq is disjoint_valued ; ::_thesis: ASeq is V73()
for m, n being Element of NAT st m <> n holds
ASeq . m misses ASeq . n
proof
let m, n be Element of NAT ; ::_thesis: ( m <> n implies ASeq . m misses ASeq . n )
assume A6: m <> n ; ::_thesis: ASeq . m misses ASeq . n
percases ( ( m in dom FSeq & n in dom FSeq ) or not m in dom FSeq or not n in dom FSeq ) ;
supposeA7: ( m in dom FSeq & n in dom FSeq ) ; ::_thesis: ASeq . m misses ASeq . n
FSeq . m misses FSeq . n by A5, A6, PROB_2:def_2;
then ASeq . m misses FSeq . n by A1, A7;
hence ASeq . m misses ASeq . n by A1, A7; ::_thesis: verum
end;
suppose ( not m in dom FSeq or not n in dom FSeq ) ; ::_thesis: ASeq . m misses ASeq . n
then ( ASeq . m = {} or ASeq . n = {} ) by A2;
hence ASeq . m misses ASeq . n by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence ASeq is V73() by PROB_2:def_3; ::_thesis: verum
end;
thus P . (Union FSeq) = P . (Union ASeq) by A1, A2, Th55
.= Sum (P * ASeq) by A4, A3, Th46
.= Sum (P * FSeq) by A1, A2, Th64 ; ::_thesis: verum
end;
definition
canceled;
canceled;
let X be set ;
let IT be Subset-Family of X;
attrIT 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;
attrIT 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
let X be set ; ::_thesis: 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 )
let IT be Subset-Family of X; ::_thesis: ( 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 )
thus ( IT is non-decreasing-closed implies for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
lim A1 in IT ) ::_thesis: ( ( for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
lim A1 in IT ) implies IT is non-decreasing-closed )
proof
assume A1: IT is non-decreasing-closed ; ::_thesis: for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
lim A1 in IT
now__::_thesis:_for_A1_being_SetSequence_of_X_st_A1_is_V71()_&_rng_A1_c=_IT_holds_
lim_A1_in_IT
let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= IT implies lim A1 in IT )
assume that
A2: A1 is V71() and
A3: rng A1 c= IT ; ::_thesis: lim A1 in IT
Union A1 in IT by A1, A2, A3, Def9;
hence lim A1 in IT by A2, SETLIM_1:63; ::_thesis: verum
end;
hence for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
lim A1 in IT ; ::_thesis: verum
end;
assume A4: for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
lim A1 in IT ; ::_thesis: IT is non-decreasing-closed
for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds
Union A1 in IT
proof
let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= IT implies Union A1 in IT )
assume that
A5: A1 is V71() and
A6: rng A1 c= IT ; ::_thesis: Union A1 in IT
lim A1 in IT by A4, A5, A6;
hence Union A1 in IT by A5, SETLIM_1:63; ::_thesis: verum
end;
hence IT is non-decreasing-closed by Def9; ::_thesis: verum
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
let X be set ; ::_thesis: 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 )
let IT be Subset-Family of X; ::_thesis: ( 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 )
thus ( IT is non-increasing-closed implies for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
lim A1 in IT ) ::_thesis: ( ( for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
lim A1 in IT ) implies IT is non-increasing-closed )
proof
assume A1: IT is non-increasing-closed ; ::_thesis: for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
lim A1 in IT
now__::_thesis:_for_A1_being_SetSequence_of_X_st_A1_is_V70()_&_rng_A1_c=_IT_holds_
lim_A1_in_IT
let A1 be SetSequence of X; ::_thesis: ( A1 is V70() & rng A1 c= IT implies lim A1 in IT )
assume that
A2: A1 is V70() and
A3: rng A1 c= IT ; ::_thesis: lim A1 in IT
Intersection A1 in IT by A1, A2, A3, Def10;
hence lim A1 in IT by A2, SETLIM_1:64; ::_thesis: verum
end;
hence for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
lim A1 in IT ; ::_thesis: verum
end;
assume A4: for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
lim A1 in IT ; ::_thesis: IT is non-increasing-closed
for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds
Intersection A1 in IT
proof
let A1 be SetSequence of X; ::_thesis: ( A1 is V70() & rng A1 c= IT implies Intersection A1 in IT )
assume that
A5: A1 is V70() and
A6: rng A1 c= IT ; ::_thesis: Intersection A1 in IT
lim A1 in IT by A4, A5, A6;
hence Intersection A1 in IT by A5, SETLIM_1:64; ::_thesis: verum
end;
hence IT is non-increasing-closed by Def10; ::_thesis: verum
end;
theorem Th68: :: PROB_3:68
for X being set holds
( bool X is non-decreasing-closed & bool X is non-increasing-closed )
proof
let X be set ; ::_thesis: ( bool X is non-decreasing-closed & bool X is non-increasing-closed )
for A1 being SetSequence of X st A1 is V71() & rng A1 c= bool X holds
Union A1 in bool X ;
hence bool X is non-decreasing-closed by Def9; ::_thesis: bool X is non-increasing-closed
for A1 being SetSequence of X st A1 is V70() & rng A1 c= bool X holds
Intersection A1 in bool X ;
hence bool X is non-increasing-closed by Def10; ::_thesis: verum
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
take bool X ; ::_thesis: ( bool X is non-decreasing-closed & bool X is non-increasing-closed )
thus ( bool X is non-decreasing-closed & bool X is non-increasing-closed ) by Th68; ::_thesis: verum
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
let Z, X be set ; ::_thesis: ( 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 ) ) )
thus ( Z is MonotoneClass of X implies ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) ) ::_thesis: ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) implies Z is MonotoneClass of X )
proof
assume A1: Z is MonotoneClass of X ; ::_thesis: ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) )
then reconsider Z = Z as Subset-Family of X ;
for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X; ::_thesis: ( A1 is monotone & rng A1 c= Z implies lim A1 in Z )
assume that
A2: A1 is monotone and
A3: rng A1 c= Z ; ::_thesis: lim A1 in Z
percases ( not A1 is V71() or not A1 is V70() ) by A2, SETLIM_1:def_1;
suppose A1 is V71() ; ::_thesis: lim A1 in Z
hence lim A1 in Z by A1, A3, Th66; ::_thesis: verum
end;
suppose A1 is V70() ; ::_thesis: lim A1 in Z
hence lim A1 in Z by A1, A3, Th67; ::_thesis: verum
end;
end;
end;
hence ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) ; ::_thesis: verum
end;
assume that
A4: Z c= bool X and
A5: for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ; ::_thesis: Z is MonotoneClass of X
reconsider Z = Z as Subset-Family of X by A4;
A6: for A1 being SetSequence of X st A1 is V70() & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X; ::_thesis: ( A1 is V70() & rng A1 c= Z implies lim A1 in Z )
assume A7: ( A1 is V70() & rng A1 c= Z ) ; ::_thesis: lim A1 in Z
( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) by A5;
hence lim A1 in Z by A7, SETLIM_1:def_1; ::_thesis: verum
end;
for A1 being SetSequence of X st A1 is V71() & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= Z implies lim A1 in Z )
assume A8: ( A1 is V71() & rng A1 c= Z ) ; ::_thesis: lim A1 in Z
( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) by A5;
hence lim A1 in Z by A8, SETLIM_1:def_1; ::_thesis: verum
end;
hence Z is MonotoneClass of X by A6, Th66, Th67; ::_thesis: verum
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
let X be set ; ::_thesis: for F being Field_Subset of X holds
( F is SigmaField of X iff F is MonotoneClass of X )
let F be Field_Subset of X; ::_thesis: ( F is SigmaField of X iff F is MonotoneClass of X )
thus ( F is SigmaField of X implies F is MonotoneClass of X ) ::_thesis: ( F is MonotoneClass of X implies F is SigmaField of X )
proof
assume F is SigmaField of X ; ::_thesis: F is MonotoneClass of X
then reconsider F = F as SigmaField of X ;
A1: for A1 being SetSequence of X st A1 is V71() & rng A1 c= F holds
Union A1 in F
proof
let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= F implies Union A1 in F )
assume that
A1 is V71() and
A2: rng A1 c= F ; ::_thesis: Union A1 in F
reconsider A2 = A1 as SetSequence of F by A2, RELAT_1:def_19;
Union A2 in F by PROB_1:17;
hence Union A1 in F ; ::_thesis: verum
end;
F is non-increasing-closed
proof
let A1 be SetSequence of X; :: according to PROB_3:def_10 ::_thesis: ( A1 is V70() & rng A1 c= F implies Intersection A1 in F )
assume A1 is V70() ; ::_thesis: ( not rng A1 c= F or Intersection A1 in F )
assume rng A1 c= F ; ::_thesis: Intersection A1 in F
hence Intersection A1 in F by PROB_1:def_6; ::_thesis: verum
end;
hence F is MonotoneClass of X by A1, Def9; ::_thesis: verum
end;
assume A3: F is MonotoneClass of X ; ::_thesis: F is SigmaField of X
for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F
proof
let A1 be SetSequence of X; ::_thesis: ( rng A1 c= F implies Intersection A1 in F )
assume A4: rng A1 c= F ; ::_thesis: Intersection A1 in F
set A2 = Partial_Intersection A1;
defpred S1[ Nat] means (Partial_Intersection A1) . $1 in F;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: (Partial_Intersection A1) . k in F ; ::_thesis: S1[k + 1]
( A1 . (k + 1) in rng A1 & (Partial_Intersection A1) . (k + 1) = ((Partial_Intersection A1) . k) /\ (A1 . (k + 1)) ) by Def1, NAT_1:51;
hence (Partial_Intersection A1) . (k + 1) in F by A4, A6, FINSUB_1:def_2; ::_thesis: verum
end;
( A1 . 0 in rng A1 & (Partial_Intersection A1) . 0 = A1 . 0 ) by Def1, NAT_1:51;
then A7: S1[ 0 ] by A4;
for k being Nat holds S1[k] from NAT_1:sch_2(A7, A5);
then A8: rng (Partial_Intersection A1) c= F by NAT_1:52;
Partial_Intersection A1 is V70() by Th10;
then Intersection (Partial_Intersection A1) in F by A3, A8, Def10;
hence Intersection A1 in F by Th14; ::_thesis: verum
end;
hence F is SigmaField of X by PROB_1:def_6; ::_thesis: verum
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
set V = { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
set Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
A1: for Z being set st Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds
X c= Z
proof
let Z be set ; ::_thesis: ( Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies X c= Z )
assume Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; ::_thesis: X c= Z
then ex M being Subset-Family of Omega st
( Z = M & X c= M & M is MonotoneClass of Omega ) ;
hence X c= Z ; ::_thesis: verum
end;
bool Omega is MonotoneClass of Omega by Th68;
then A2: bool Omega in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
for MSeq being SetSequence of Omega st MSeq is monotone & rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds
lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) }
proof
let MSeq be SetSequence of Omega; ::_thesis: ( MSeq is monotone & rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } )
assume that
A3: MSeq is monotone and
A4: rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; ::_thesis: lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) }
now__::_thesis:_for_Z_being_set_st_Z_in__{__M_where_M_is_Subset-Family_of_Omega_:_(_X_c=_M_&_M_is_MonotoneClass_of_Omega_)__}__holds_
lim_MSeq_in_Z
let Z be set ; ::_thesis: ( Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies lim MSeq in Z )
assume A5: Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; ::_thesis: lim MSeq in Z
now__::_thesis:_for_n_being_Nat_holds_MSeq_._n_in_Z
let n be Nat; ::_thesis: MSeq . n in Z
MSeq . n in rng MSeq by NAT_1:51;
hence MSeq . n in Z by A4, A5, SETFAM_1:def_1; ::_thesis: verum
end;
then A6: rng MSeq c= Z by NAT_1:52;
ex M being Subset-Family of Omega st
( Z = M & X c= M & M is MonotoneClass of Omega ) by A5;
hence lim MSeq in Z by A3, A6, Th69; ::_thesis: verum
end;
hence lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } as MonotoneClass of Omega by A2, Th69, SETFAM_1:3;
take Y ; ::_thesis: ( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) )
for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z
proof
let Z be set ; ::_thesis: ( X c= Z & Z is MonotoneClass of Omega implies Y c= Z )
assume ( X c= Z & Z is MonotoneClass of Omega ) ; ::_thesis: Y c= Z
then Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
hence Y c= Z by SETFAM_1:3; ::_thesis: verum
end;
hence ( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) ) by A2, A1, SETFAM_1:5; ::_thesis: verum
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
let R1, R2 be MonotoneClass of Omega; ::_thesis: ( X c= R1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R2 c= Z ) implies R1 = R2 )
assume that
A7: X c= R1 and
A8: ( ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R1 c= Z ) & X c= R2 ) and
A9: for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R2 c= Z ; ::_thesis: R1 = R2
thus R1 c= R2 by A8; :: according to XBOOLE_0:def_10 ::_thesis: R2 c= R1
thus R2 c= R1 by A7, A9; ::_thesis: verum
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
let Omega be non empty set ; ::_thesis: for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega
let Z be Field_Subset of Omega; ::_thesis: monotoneclass Z is Field_Subset of Omega
A1: Z c= monotoneclass Z by Def11;
then reconsider Z1 = monotoneclass Z as non empty Subset-Family of Omega ;
A2: for y, Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
proof
let y, Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) )
assume A3: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
thus for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ::_thesis: verum
proof
let z be set ; ::_thesis: ( z in Y implies ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) )
assume z in Y ; ::_thesis: ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
then ex z1 being Element of Z1 st
( z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 ) by A3;
hence ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ; ::_thesis: verum
end;
end;
A4: for y being Element of Z1
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Y is MonotoneClass of Omega
proof
let y be Element of Z1; ::_thesis: for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Y is MonotoneClass of Omega
let Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Y is MonotoneClass of Omega )
assume A5: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: Y is MonotoneClass of Omega
A6: for A1 being SetSequence of Omega st A1 is monotone & rng A1 c= Y holds
lim A1 in Y
proof
let A1 be SetSequence of Omega; ::_thesis: ( A1 is monotone & rng A1 c= Y implies lim A1 in Y )
assume that
A7: A1 is monotone and
A8: rng A1 c= Y ; ::_thesis: lim A1 in Y
A9: A1 is convergent by A7, SETLIM_1:65;
for n being Nat holds A1 . n in Z1
proof
let n be Nat; ::_thesis: A1 . n in Z1
A1 . n in rng A1 by NAT_1:51;
hence A1 . n in Z1 by A2, A5, A8; ::_thesis: verum
end;
then rng A1 c= Z1 by NAT_1:52;
then A10: lim A1 is Element of Z1 by A7, Th69;
for n being Nat holds (A1 (\) y) . n in Z1
proof
let n be Nat; ::_thesis: (A1 (\) y) . n in Z1
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & (A1 . n) \ y in Z1 ) by A2, A5, A8, ORDINAL1:def_12;
hence (A1 (\) y) . n in Z1 by SETLIM_2:def_8; ::_thesis: verum
end;
then A11: rng (A1 (\) y) c= Z1 by NAT_1:52;
for n being Nat holds (y (/\) A1) . n in Z1
proof
let n be Nat; ::_thesis: (y (/\) A1) . n in Z1
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & y /\ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def_12;
hence (y (/\) A1) . n in Z1 by SETLIM_2:def_5; ::_thesis: verum
end;
then A12: rng (y (/\) A1) c= Z1 by NAT_1:52;
y (/\) A1 is monotone by A7, SETLIM_2:23;
then lim (y (/\) A1) in Z1 by A12, Th69;
then A13: y /\ (lim A1) in Z1 by A9, SETLIM_2:92;
for n being Nat holds (y (\) A1) . n in Z1
proof
let n be Nat; ::_thesis: (y (\) A1) . n in Z1
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & y \ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def_12;
hence (y (\) A1) . n in Z1 by SETLIM_2:def_7; ::_thesis: verum
end;
then A14: rng (y (\) A1) c= Z1 by NAT_1:52;
y (\) A1 is monotone by A7, SETLIM_2:29;
then lim (y (\) A1) in Z1 by A14, Th69;
then A15: y \ (lim A1) in Z1 by A9, SETLIM_2:94;
A1 (\) y is monotone by A7, SETLIM_2:32;
then lim (A1 (\) y) in Z1 by A11, Th69;
then (lim A1) \ y in Z1 by A9, SETLIM_2:95;
hence lim A1 in Y by A5, A10, A15, A13; ::_thesis: verum
end;
for z being set st z in Y holds
z in Z1 by A2, A5;
then Y c= Z1 by TARSKI:def_3;
hence Y is MonotoneClass of Omega by A6, Th69, XBOOLE_1:1; ::_thesis: verum
end;
A16: for y being Element of Z
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
proof
let y be Element of Z; ::_thesis: for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
let Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )
assume A17: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: Z1 c= Y
A18: Z c= Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y )
assume A19: z in Z ; ::_thesis: z in Y
then A20: z /\ y in Z by FINSUB_1:def_2;
( z \ y in Z & y \ z in Z ) by A19, PROB_1:6;
hence z in Y by A1, A17, A19, A20; ::_thesis: verum
end;
y in Z ;
then Y is MonotoneClass of Omega by A1, A4, A17;
hence Z1 c= Y by A18, Def11; ::_thesis: verum
end;
A21: for y being Element of Z1
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
proof
let y be Element of Z1; ::_thesis: for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
let Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )
assume A22: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: Z1 c= Y
A23: Z c= Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y )
set Y1 = { x where x is Element of Z1 : ( z \ x in Z1 & x \ z in Z1 & x /\ z in Z1 ) } ;
assume A24: z in Z ; ::_thesis: z in Y
then A25: Z1 c= { x where x is Element of Z1 : ( z \ x in Z1 & x \ z in Z1 & x /\ z in Z1 ) } by A16;
A26: y in Z1 ;
then A27: z /\ y in Z1 by A2, A25;
( z \ y in Z1 & y \ z in Z1 ) by A2, A25, A26;
hence z in Y by A1, A22, A24, A27; ::_thesis: verum
end;
Y is MonotoneClass of Omega by A4, A22;
hence Z1 c= Y by A23, Def11; ::_thesis: verum
end;
A28: for y being Subset of Omega st y in Z1 holds
y ` in Z1
proof
Omega in Z by PROB_1:5;
then A29: Omega in Z1 by A1;
let y be Subset of Omega; ::_thesis: ( y in Z1 implies y ` in Z1 )
assume A30: y in Z1 ; ::_thesis: y ` in Z1
set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;
Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A30;
then Omega \ y in Z1 by A2, A29;
hence y ` in Z1 by SUBSET_1:def_4; ::_thesis: verum
end;
now__::_thesis:_for_y,_z_being_set_st_y_in_Z1_&_z_in_Z1_holds_
y_/\_z_in_Z1
let y, z be set ; ::_thesis: ( y in Z1 & z in Z1 implies y /\ z in Z1 )
assume that
A31: y in Z1 and
A32: z in Z1 ; ::_thesis: y /\ z in Z1
set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;
Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A31;
hence y /\ z in Z1 by A2, A32; ::_thesis: verum
end;
hence monotoneclass Z is Field_Subset of Omega by A28, FINSUB_1:def_2, PROB_1:def_1; ::_thesis: verum
end;
theorem :: PROB_3:73
for Omega being non empty set
for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z
proof
let Omega be non empty set ; ::_thesis: for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z
let Z be Field_Subset of Omega; ::_thesis: sigma Z = monotoneclass Z
monotoneclass Z is Field_Subset of Omega by Th72;
then A1: monotoneclass Z is SigmaField of Omega by Th70;
Z c= monotoneclass Z by Def11;
hence sigma Z c= monotoneclass Z by A1, PROB_1:def_9; :: according to XBOOLE_0:def_10 ::_thesis: monotoneclass Z c= sigma Z
( sigma Z is MonotoneClass of Omega & Z c= sigma Z ) by Th70, PROB_1:def_9;
hence monotoneclass Z c= sigma Z by Def11; ::_thesis: verum
end;