@[reducible, inline]

abbrev DiscreteFiltration (Ω : Type u_1) (m : MeasurableSpace Ω) : Type u_1

Discrete-time filtration. An increasing sequence of sub-σ-algebras (ℱ_n)_{n ∈ ℕ} of m. Abbreviation for Filtration ℕ m.