let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds
Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)
let Sigma be SigmaField of Omega; :: thesis: for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds
Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)
let S be non empty Subset of REAL; :: thesis: for MyFunc being Filtration of S,Sigma
for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds
Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)
let MyFunc be Filtration of S,Sigma; :: thesis: for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds
Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)
let k1, k2 be StoppingTime_Func of Sigma,MyFunc; :: thesis: ( k1 <= k2 implies Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2) )
assume ASS0: k1 <= k2 ; :: thesis: Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sigma_tau (MyFunc,k1) or x in Sigma_tau (MyFunc,k2) )
assume x in Sigma_tau (MyFunc,k1) ; :: thesis: x in Sigma_tau (MyFunc,k2)
then consider A being Element of Sigma such that
Z1: ( x = A & ( for t being Element of S holds A /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } in MyFunc . t ) ) ;
reconsider x = x as Element of Sigma by Z1;
for t being Element of S holds x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } in MyFunc . t
proof
let t be Element of S; :: thesis: x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } in MyFunc . t
reconsider MyFt = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
set Imp0 = { w2 where w2 is Element of Omega : k2 . w2 <= t } ;
set Imp1 = x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ;
set Imp2 = (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ;
BU2: x /\ { w where w is Element of Omega : k1 . w <= t } is Event of MyFt by Z1;
P1: x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } = (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }
proof
thus x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } c= (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } :: according to XBOOLE_0:def 10 :: thesis: (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } c= x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } or y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } )
assume zw1: y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ; :: thesis: y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }
then ZW1: ( y in x & y in { w where w is Element of Omega : k2 . w <= t } ) by XBOOLE_0:def 4;
then consider w2 being Element of Omega such that
ZW2: ( y = w2 & k2 . w2 <= t ) ;
( k1 . w2 <= k2 . w2 & k2 . w2 <= t ) by ZW2, ASS0;
then k1 . w2 <= t by XXREAL_0:2;
then ( y in x & y in { w where w is Element of Omega : k1 . w <= t } ) by ZW2, zw1, XBOOLE_0:def 4;
then y in x /\ { w where w is Element of Omega : k1 . w <= t } by XBOOLE_0:def 4;
hence y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } by ZW1, XBOOLE_0:def 4; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } or y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } )
assume y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ; :: thesis: y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }
then ( y in x /\ { w where w is Element of Omega : k1 . w <= t } & y in { w2 where w2 is Element of Omega : k2 . w2 <= t } ) by XBOOLE_0:def 4;
then ( y in x & y in { w where w is Element of Omega : k1 . w <= t } & y in { w where w is Element of Omega : k2 . w <= t } ) by XBOOLE_0:def 4;
hence y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } by XBOOLE_0:def 4; :: thesis: verum
end;
x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } is Event of MyFt
proof
k2 is_StoppingTime_wrt MyFunc,S by Def11111;
then { w where w is Element of Omega : k2 . w <= t } is Event of MyFt ;
hence x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } is Event of MyFt by P1, BU2, PROB_1:19; :: thesis: verum
end;
hence x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } in MyFunc . t ; :: thesis: verum
end;
hence x in Sigma_tau (MyFunc,k2) ; :: thesis: verum