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)

k3 is_StoppingTime_wrt MyFunc,T

( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: verum

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

then reconsider k3 = min (k1,k2) as Function of Omega,(StoppingSetExt T) ;
rng (min (k1,k2)) c= StoppingSetExt T

hence min (k1,k2) is Function of Omega,(StoppingSetExt T) by FUNCT_2:def 1; :: thesis: verum

end;proof

then
min (k1,k2) is Function of (dom (min (k1,k2))),(StoppingSetExt T)
by FUNCT_2:2;
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

end;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
end;

hence
x in StoppingSetExt T
by Def21, C1; :: thesis: verumper cases
( not k2 . x2 <= k1 . x2 or k2 . x2 <= k1 . x2 )
;

end;

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;hence min ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW1; :: thesis: verum

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;hence min ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW2; :: thesis: verum

hence min (k1,k2) is Function of Omega,(StoppingSetExt T) by FUNCT_2:def 1; :: thesis: verum

k3 is_StoppingTime_wrt MyFunc,T

proof

hence
ex k3 being Function of Omega,(StoppingSetExt T) st
for t being Element of StoppingSet T holds { w where w is Element of Omega : k3 . w <= t } in MyFunc . t

end;proof

hence
k3 is_StoppingTime_wrt MyFunc,T
by KJK; :: thesis: verum
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 ) }

end;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

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 }
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 ) } )

end;( 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

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
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 } )

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;

end;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 : ( k2 . w <= t or k1 . w <= t ) }
; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }
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;

end;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 )
;

end;

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;

end;

suppose S1J:
k2 . w2 <= t
; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }

min ((k1 . w2),(k2 . w2)) <= t

end;proof
end;

hence
x in { w where w is Element of Omega : k3 . w <= t }
by R1, HHH; :: thesis: verumsuppose S1J:
k1 . w2 <= t
; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }

min ((k1 . w2),(k2 . w2)) <= t

end;proof
end;

hence
x in { w where w is Element of Omega : k3 . w <= t }
by R1, HHH; :: thesis: verumper cases
( k1 . w2 <= k2 . w2 or not k1 . w2 <= k2 . w2 )
;

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;hence min ((k1 . w2),(k2 . w2)) <= t by QS, S1J, XXREAL_0:2; :: thesis: verum

proof

{ w where w is Element of Omega : k2 . w <= t } \/ { w where w is Element of Omega : k1 . w <= t } in MyFunc . t
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 } )

end;( 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

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
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 ) } )

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;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 } \/ { 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 ) }
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;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

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

proof

hence
{ w where w is Element of Omega : k3 . w <= t } in MyFunc . t
by O2, O1; :: thesis: verum
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;( { 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

( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: verum