set MySigmatau = { A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } ;
{ A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } c= bool Omega
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } or x in bool Omega )
assume x in { A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } ; :: thesis: x in bool Omega
then ex A being Element of Sigma st
( x = A & ( for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t ) ) ;
hence x in bool Omega ; :: thesis: verum
end;
then reconsider MySigmatau = { A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } as Subset-Family of Omega ;
A1: MySigmatau is compl-closed
proof
for A being Subset of Omega st A in MySigmatau holds
A ` in MySigmatau
proof
let A be Subset of Omega; :: thesis: ( A in MySigmatau implies A ` in MySigmatau )
assume A in MySigmatau ; :: thesis: A ` in MySigmatau
then consider B being Element of Sigma such that
GW1: ( A = B & ( for t being Element of I holds B /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t ) ) ;
reconsider A = A as Element of Sigma by GW1;
GW2: for t being Element of I holds (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
proof
let t be Element of I; :: thesis: (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
reconsider MyFt2 = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
WW0: for j being object st j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) holds
j in (A `) /\ { w where w is Element of Omega : tau . w <= t }
proof
let j be object ; :: thesis: ( j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) implies j in (A `) /\ { w where w is Element of Omega : tau . w <= t } )
assume h: j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) ; :: thesis: j in (A `) /\ { w where w is Element of Omega : tau . w <= t }
then Help00: ( j in { w where w is Element of Omega : tau . w <= t } & not j in A /\ { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 5;
then Help2: not j in A by XBOOLE_0:def 4;
j in A `
proof
ex w2 being Element of Omega st
( j = w2 & tau . w2 <= t ) by Help00;
hence j in A ` by ; :: thesis: verum
end;
hence j in (A `) /\ { w where w is Element of Omega : tau . w <= t } by ; :: thesis: verum
end;
E1: { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) = (A `) /\ { w where w is Element of Omega : tau . w <= t }
proof
for j being object st j in (A `) /\ { w where w is Element of Omega : tau . w <= t } holds
j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } )
proof
let j be object ; :: thesis: ( j in (A `) /\ { w where w is Element of Omega : tau . w <= t } implies j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) )
assume j in (A `) /\ { w where w is Element of Omega : tau . w <= t } ; :: thesis: j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } )
then hh: ( j in Omega \ A & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;
then ( j in Omega & not j in A & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 5;
then not j in A /\ { w where w is Element of Omega : tau . w <= t } by XBOOLE_0:def 4;
hence j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) by ; :: thesis: verum
end;
hence { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) = (A `) /\ { w where w is Element of Omega : tau . w <= t } by ; :: thesis: verum
end;
W2: A /\ { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 by GW1;
tau is_StoppingTime_wrt MyFunc by Def1111;
then { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 ;
then { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) is Event of MyFt2 by ;
hence (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by E1; :: thesis: verum
end;
( Omega in Sigma & A in Sigma ) by PROB_1:5;
then Omega \ A in Sigma by PROB_1:6;
hence A ` in MySigmatau by GW2; :: thesis: verum
end;
hence MySigmatau is compl-closed ; :: thesis: verum
end;
A2: MySigmatau is sigma-multiplicative
proof
let A1 be SetSequence of Omega; :: according to PROB_1:def 6 :: thesis: ( not rng A1 c= MySigmatau or Intersection A1 in MySigmatau )
assume ASSJ: rng A1 c= MySigmatau ; :: thesis: Intersection A1 in MySigmatau
TT1: for n being Nat holds A1 . n in MySigmatau
proof
let n be Nat; :: thesis: A1 . n in MySigmatau
A1 . n in rng A1 by ;
hence A1 . n in MySigmatau by ASSJ; :: thesis: verum
end;
QQ1: for t being Element of I holds (Union ()) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
proof
let t be Element of I; :: thesis: (Union ()) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
X1: for x being object st x in Union (Sigma_tauhelp3 (tau,A1,t)) holds
x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t }
proof
let x be object ; :: thesis: ( x in Union (Sigma_tauhelp3 (tau,A1,t)) implies x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t } )
assume x in Union (Sigma_tauhelp3 (tau,A1,t)) ; :: thesis: x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t }
then consider n being Nat such that
V1: x in (Sigma_tauhelp3 (tau,A1,t)) . n by PROB_1:12;
x in Sigma_tauhelp2 (tau,A1,n,t) by ;
then x in (() . n) /\ { w where w is Element of Omega : tau . w <= t } by ;
then ZWJ1: ( x in () . n & x in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;
x in Union () by ;
hence x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t } by ; :: thesis: verum
end;
H: for x being object st x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t } holds
x in Union (Sigma_tauhelp3 (tau,A1,t))
proof
let x be object ; :: thesis: ( x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t } implies x in Union (Sigma_tauhelp3 (tau,A1,t)) )
assume x in (Union ()) /\ { w where w is Element of Omega : tau . w <= t } ; :: thesis: x in Union (Sigma_tauhelp3 (tau,A1,t))
then ZWJ1: ( x in Union () & x in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;
then consider n being Nat such that
ZWJ2: x in () . n by PROB_1:12;
x in (() . n) /\ { w where w is Element of Omega : tau . w <= t } by ;
then ZWJ2: x in Sigma_tauhelp2 (tau,A1,n,t) by ;
x in (Sigma_tauhelp3 (tau,A1,t)) . n by ;
hence x in Union (Sigma_tauhelp3 (tau,A1,t)) by PROB_1:12; :: thesis: verum
end;
Union (Sigma_tauhelp3 (tau,A1,t)) = (Union ()) /\ { w where w is Element of Omega : tau . w <= t } by ;
hence (Union ()) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by PROB_1:17; :: thesis: verum
end;
for n being Nat holds A1 . n is Event of Sigma
proof
let n be Nat; :: thesis: A1 . n is Event of Sigma
A1 . n in MySigmatau by TT1;
then ex AJ being Element of Sigma st
( AJ = A1 . n & ( for t being Element of I holds AJ /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) ;
hence A1 . n is Event of Sigma ; :: thesis: verum
end;
then reconsider A1 = A1 as SetSequence of Sigma by PROB_1:25;
set CA = Complement A1;
for n being Nat holds () . n is Event of Sigma
proof
let n be Nat; :: thesis: () . n is Event of Sigma
A1 . n in MySigmatau by TT1;
then consider AJ being Element of Sigma such that
AB1: ( AJ = A1 . n & ( for t being Element of I holds AJ /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) ;
( A1 . n is Event of Sigma & Sigma is compl-closed ) by AB1;
then (A1 . n) ` is Event of Sigma ;
hence (Complement A1) . n is Event of Sigma by PROB_1:def 2; :: thesis: verum
end;
then reconsider CA = Complement A1 as SetSequence of Sigma by PROB_1:25;
reconsider UCA = Union CA as Event of Sigma by PROB_1:26;
UCA in MySigmatau by QQ1;
hence Intersection A1 in MySigmatau by A1; :: thesis: verum
end;
K1: for t being Element of I holds Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t
proof
let t be Element of I; :: thesis: Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t
tau is MyFunc -StoppingTime-like ;
then tau is_StoppingTime_wrt MyFunc ;
then N1: { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ;
reconsider MyFt = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
Omega is Event of MyFt by PROB_1:5;
then Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } is Event of MyFt by ;
hence Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ; :: thesis: verum
end;
( Omega is Element of Sigma & ( for t being Element of I holds Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) by ;
then Omega in MySigmatau ;
hence { A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } is SigmaField of Omega by A1, A2; :: thesis: verum