measurableSet_le — Mathlib

English

If hτ is a stopping time, then for every i, the set {ω | τ(ω) ≤ i} is measurable in the i-th filtration.

Русский

Если hτ — время останова, то для каждого i множество {ω | τ(ω) ≤ i} измеримо в f_i.

LaTeX

$$$$ \text{If } h_\tau \text{ is a stopping time, then } \{\omega \mid \tau(\omega) \le i\} \in \mathcal F_i. $$$$

Lean4

protected theorem measurableSet_le (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[f i] {ω | τ ω ≤ i} :=
  hτ i

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