let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let Sigma be SigmaField of Omega; :: thesis: for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let T be Nat; :: thesis: for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis: for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let k1, k2 be Function of Omega,(StoppingSetExt T); :: thesis: ( k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T implies ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) )
assume ASS: ( k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
set k3 = min (k1,k2);
min (k1,k2) is Function of Omega,(StoppingSetExt T)
proof
rng (min (k1,k2)) c= StoppingSetExt T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (min (k1,k2)) or x in StoppingSetExt T )
assume x in rng (min (k1,k2)) ; :: thesis: x in StoppingSetExt T
then consider x2 being object such that
C1: ( x2 in dom (min (k1,k2)) & x = (min (k1,k2)) . x2 ) by FUNCT_1:def 3;
O1: x2 in Omega by C1;
then x2 in dom k1 by FUNCT_2:def 1;
then ZW1: k1 . x2 in rng k1 by FUNCT_1:3;
x2 in dom k2 by O1, FUNCT_2:def 1;
then ZW2: k2 . x2 in rng k2 by FUNCT_1:3;
min ((k1 . x2),(k2 . x2)) in StoppingSetExt T
proof
per cases ( not k2 . x2 <= k1 . x2 or k2 . x2 <= k1 . x2 ) ;
suppose not k2 . x2 <= k1 . x2 ; :: thesis: min ((k1 . x2),(k2 . x2)) in StoppingSetExt T
then k1 . x2 = min ((k1 . x2),(k2 . x2)) by XXREAL_0:def 9;
hence min ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW1; :: thesis: verum
end;
suppose k2 . x2 <= k1 . x2 ; :: thesis: min ((k1 . x2),(k2 . x2)) in StoppingSetExt T
then k2 . x2 = min ((k1 . x2),(k2 . x2)) by XXREAL_0:def 9;
hence min ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW2; :: thesis: verum
end;
end;
end;
hence x in StoppingSetExt T by Def21, C1; :: thesis: verum
end;
then min (k1,k2) is Function of (dom (min (k1,k2))),(StoppingSetExt T) by FUNCT_2:2;
hence min (k1,k2) is Function of Omega,(StoppingSetExt T) by FUNCT_2:def 1; :: thesis: verum
end;
then reconsider k3 = min (k1,k2) as Function of Omega,(StoppingSetExt T) ;
k3 is_StoppingTime_wrt MyFunc,T
proof
for t being Element of StoppingSet T holds { w where w is Element of Omega : k3 . w <= t } in MyFunc . t
proof
let t be Element of StoppingSet T; :: thesis: { w where w is Element of Omega : k3 . w <= t } in MyFunc . t
O1: { w where w is Element of Omega : k3 . w <= t } = { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) }
proof
for x being object holds
( x in { w where w is Element of Omega : k3 . w <= t } iff x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : k3 . w <= t } iff x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } )
thus ( x in { w where w is Element of Omega : k3 . w <= t } implies x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } ) :: thesis: ( x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } implies x in { w where w is Element of Omega : k3 . w <= t } )
proof
assume x in { w where w is Element of Omega : k3 . w <= t } ; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) }
then consider w2 being Element of Omega such that
R1: ( x = w2 & k3 . w2 <= t ) ;
HHH: k3 . w2 = min ((k1 . w2),(k2 . w2)) by Def21;
set K3 = k3 . w2;
set K1 = k1 . w2;
set K2 = k2 . w2;
per cases ( k1 . w2 > k2 . w2 or k1 . w2 <= k2 . w2 ) ;
suppose k1 . w2 > k2 . w2 ; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) }
then k3 . w2 = k2 . w2 by HHH, XXREAL_0:def 9;
hence x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } by R1; :: thesis: verum
end;
suppose k1 . w2 <= k2 . w2 ; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) }
then k3 . w2 = k1 . w2 by HHH, XXREAL_0:def 9;
hence x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } by R1; :: thesis: verum
end;
end;
end;
assume x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } ; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }
then consider w2 being Element of Omega such that
R1: ( x = w2 & ( k2 . w2 <= t or k1 . w2 <= t ) ) ;
HHH: k3 . w2 = min ((k1 . w2),(k2 . w2)) by Def21;
per cases ( k2 . w2 <= t or k1 . w2 <= t ) by R1;
suppose S1J: k2 . w2 <= t ; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }
min ((k1 . w2),(k2 . w2)) <= t
proof
per cases ( k1 . w2 <= k2 . w2 or k1 . w2 > k2 . w2 ) ;
suppose QS: k1 . w2 <= k2 . w2 ; :: thesis: min ((k1 . w2),(k2 . w2)) <= t
then min ((k1 . w2),(k2 . w2)) = k1 . w2 by XXREAL_0:def 9;
hence min ((k1 . w2),(k2 . w2)) <= t by QS, S1J, XXREAL_0:2; :: thesis: verum
end;
suppose k1 . w2 > k2 . w2 ; :: thesis: min ((k1 . w2),(k2 . w2)) <= t
hence min ((k1 . w2),(k2 . w2)) <= t by S1J, XXREAL_0:def 9; :: thesis: verum
end;
end;
end;
hence x in { w where w is Element of Omega : k3 . w <= t } by R1, HHH; :: thesis: verum
end;
suppose S1J: k1 . w2 <= t ; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }
min ((k1 . w2),(k2 . w2)) <= t
proof
per cases ( k1 . w2 <= k2 . w2 or not k1 . w2 <= k2 . w2 ) ;
suppose k1 . w2 <= k2 . w2 ; :: thesis: min ((k1 . w2),(k2 . w2)) <= t
hence min ((k1 . w2),(k2 . w2)) <= t by S1J, XXREAL_0:def 9; :: thesis: verum
end;
suppose QS: not k1 . w2 <= k2 . w2 ; :: thesis: min ((k1 . w2),(k2 . w2)) <= t
then min ((k1 . w2),(k2 . w2)) = k2 . w2 by XXREAL_0:def 9;
hence min ((k1 . w2),(k2 . w2)) <= t by QS, S1J, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence x in { w where w is Element of Omega : k3 . w <= t } by R1, HHH; :: thesis: verum
end;
end;
end;
hence { w where w is Element of Omega : k3 . w <= t } = { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } by TARSKI:2; :: thesis: verum
end;
O2: { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } = { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t }
proof
for x being object holds
( x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } iff x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } iff x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } )
thus ( x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } implies x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } ) :: thesis: ( x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } implies x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } )
proof
assume x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } ; :: thesis: x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t }
then consider w3 being Element of Omega such that
V2: ( x = w3 & ( k2 . w3 <= t or k1 . w3 <= t ) ) ;
( x in { w where w is Element of Omega : k2 . w <= t } or x in { w where w is Element of Omega : k1 . w <= t } ) by V2;
hence x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } by XBOOLE_0:def 3; :: thesis: verum
end;
assume x in { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } ; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) }
then V0: ( x in { w where w is Element of Omega : k2 . w <= t } or x in { w where w is Element of Omega : k1 . w <= t } ) by XBOOLE_0:def 3;
( ex w3 being Element of Omega st
( x = w3 & k2 . w3 <= t ) or ex w3 being Element of Omega st
( x = w3 & k1 . w3 <= t ) ) by V0;
hence x in { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } ; :: thesis: verum
end;
hence { w where w is Element of Omega : ( k2 . w <= t or k1 . w <= t ) } = { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } by TARSKI:2; :: thesis: verum
end;
{ w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } in MyFunc . t
proof
reconsider M = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
( { w where w is Element of Omega : k1 . w <= t } is Element of M & { w where w is Element of Omega : k2 . w <= t } is Element of M ) by ASS, KJK;
hence { w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } in MyFunc . t by PROB_1:3; :: thesis: verum
end;
hence { w where w is Element of Omega : k3 . w <= t } in MyFunc . t by O2, O1; :: thesis: verum
end;
hence k3 is_StoppingTime_wrt MyFunc,T by KJK; :: thesis: verum
end;
hence ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: verum