let ASeq be SetSequence of Borel_Sets ; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
A1: now :: thesis: for n being Nat holds (P * ASeq) . n = P . (ASeq . n)
let n be Nat; :: thesis: (P * ASeq) . n = P . (ASeq . n)
A2: n in NAT by ORDINAL1:def 12;
dom (P * ASeq) = NAT by FUNCT_2:def 1;
hence (P * ASeq) . n = P . (ASeq . n) by A2, FUNCT_1:12; :: thesis: verum
end;
assume A3: ASeq is non-ascending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
now :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
per cases ( for n being Nat holds 0 in ASeq . n or ex n being Nat st not 0 in ASeq . n ) ;
suppose A4: for n being Nat holds 0 in ASeq . n ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
rng ASeq c= Borel_Sets by RELAT_1:def 19;
then A5: Intersection ASeq in Borel_Sets by PROB_1:def 6;
A6: 0 in Intersection ASeq by A4, PROB_1:13;
A7: now :: thesis: for n being Nat holds (P * ASeq) . n = 1
let n be Nat; :: thesis: (P * ASeq) . n = 1
A8: ( rng ASeq c= Borel_Sets & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;
A9: ASeq . n in Borel_Sets by A8;
0 in ASeq . n by A4;
then P . (ASeq . n) = 1 by Lm1, A9;
hence (P * ASeq) . n = 1 by A1; :: thesis: verum
end;
A10: ex m being Nat st
for n being Nat st m <= n holds
(P * ASeq) . n = 1
proof
take 0 ; :: thesis: for n being Nat st 0 <= n holds
(P * ASeq) . n = 1
thus for n being Nat st 0 <= n holds
(P * ASeq) . n = 1 by A7; :: thesis: verum
end;
then lim (P * ASeq) = 1 by PROB_1:1;
hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A10, A6, A5, Lm1, PROB_1:1; :: thesis: verum
end;
suppose A11: not for n being Nat holds 0 in ASeq . n ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
rng ASeq c= Borel_Sets by RELAT_1:def 19;
then A12: Intersection ASeq in Borel_Sets by PROB_1:def 6;
A13: not 0 in Intersection ASeq by A11, PROB_1:13;
A14: ex m being Nat st
for n being Nat st m <= n holds
(P * ASeq) . n = 0
proof
consider m being Nat such that
A15: not 0 in ASeq . m by A11;
take m ; :: thesis: for n being Nat st m <= n holds
(P * ASeq) . n = 0
for n being Nat st m <= n holds
(P * ASeq) . n = 0
proof
let n be Nat; :: thesis: ( m <= n implies (P * ASeq) . n = 0 )
assume m <= n ; :: thesis: (P * ASeq) . n = 0
then ASeq . n c= ASeq . m by A3, PROB_1:def 4;
then A16: not 0 in ASeq . n by A15;
( rng ASeq c= Borel_Sets & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def 19;
then ASeq . n in Borel_Sets ;
then P . (ASeq . n) = 0 by A16, Lm1;
hence (P * ASeq) . n = 0 by A1; :: thesis: verum
end;
hence for n being Nat st m <= n holds
(P * ASeq) . n = 0 ; :: thesis: verum
end;
then lim (P * ASeq) = 0 by PROB_1:1;
hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A14, A13, A12, Lm1, PROB_1:1; :: thesis: verum
end;
end;
end;
hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ; :: thesis: verum