def IsDiscreteStoppingTime {Ω : Type u_1} {m : MeasurableSpace Ω} (f : MeasureTheory.Filtration ℕ m) (τ : Ω → WithTop ℕ) : Prop

A WithTop ℕ-valued function τ is a discrete stopping time with respect to the filtration f if for every n : ℕ, the event {ω | τ ω = n} is f n-measurable.

This is the textbook definition (Lecture 23): T is a stopping time when {T = n} ∈ ℱ_n for every n. Allowing the value ⊤ lets the stopping time be infinite.

structure DiscreteStoppingTime {Ω : Type u_1} {m : MeasurableSpace Ω} (f : MeasureTheory.Filtration ℕ m) : Type u_1

A discrete stopping time with respect to the filtration f: a WithTop ℕ-valued function bundled with a proof that it satisfies IsDiscreteStoppingTime.

• val : Ω → WithTop ℕ
• property : IsDiscreteStoppingTime f self.val