measurableSet_lt_of_countable — Mathlib

English

For countable i, the set {ω | τ(ω) < i} is measurable in F_i for a stopping time.

Русский

Для счетного i множество {ω | τ(ω) < i} измеримо в F_i для времени останова.

LaTeX

$$$$ [Countable ι] \Rightarrow \forall i, \MeasurableSet[f i] {\omega \mid τ(\omega) < i}. $$$$

Lean4

protected theorem measurableSet_lt_of_countable [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[f i] {ω | τ ω < i} :=
  hτ.measurableSet_lt_of_countable_range (Set.to_countable _) i

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