isStoppingTime_const — Mathlib

English

For any filtration f and any i, the constant stopping time τ(ω) ≡ i is a stopping time, i.e., {ω | τ(ω) ≤ i} = Ω is measurable for all i.

Русский

Для любой фильтрации f и любого i константное время останова τ(ω) ≡ i является временем останова.

LaTeX

$$$$ IsStoppingTime(f, \tau) \text{ where } \tau(\omega) = i \text{ for all } \omega. $$$$

Lean4

theorem isStoppingTime_const [Preorder ι] (f : Filtration ι m) (i : ι) : IsStoppingTime f fun _ => i := fun j => by
  simp only [MeasurableSet.const]

Похожие утверждения