measurableSet_ge_of_countable — Mathlib

English

If the index set ι is countable, then for every i, the set {ω ∈ Ω : i ≤ τ(ω)} is measurable with respect to F_i.

Русский

Если множество индексов ι счетно, то для каждого i множество {ω ∈ Ω : i ≤ τ(ω)} измеримо относительно F_i.

LaTeX

$$$\forall i, \{\omega \in \Omega \mid i \le \tau(\omega)\} \in \mathcal{F}_i$$$

Lean4

protected theorem measurableSet_ge_of_countable {ι} [LinearOrder ι] {τ : Ω → ι} {f : Filtration ι m} [Countable ι]
    (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[f i] {ω | i ≤ τ ω} :=
  hτ.measurableSet_ge_of_countable_range (Set.to_countable _) i

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