measurableSet_ge_of_countable' — Mathlib

English

Version with Countable ι: the set {ω : i ≤ τ(ω)} is measurable.

Русский

Версия для Countable ι: множество {ω : i ≤ τ(ω)} измеримо.

LaTeX

$$$\{ω : i \le τ(ω)\}$ measurable in $h_τ.measurableSpace$ for countable index set.$$

Lean4

protected theorem measurableSet_ge_of_countable' [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | i ≤ τ ω} :=
  hτ.measurableSet_ge_of_countable_range' (Set.to_countable _) i

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