@[reducible, inline]
abbrev
IsStoppingTimeContinuous
{Ω : Type u_1}
{m : MeasurableSpace Ω}
(f : MeasureTheory.Filtration NNReal m)
(S : Ω → ENNReal)
:
Continuous-time stopping time. A random variable S : Ω → [0, ∞] is a
stopping time relative to a continuous-time filtration f (indexed by ℝ≥0) when
the event {S > t} lies in f t for every t ≥ 0. This is the continuous-time
analogue used for Brownian motion and related processes.