measurableSet_lt_of_countable_range

English

If hτ is a stopping time and τ has countable range, then for any i, the set {ω | τ(ω) < i} is measurable in F_i.

Русский

Если hτ — время останова и диапазон τ счетен, то для любого i множество {ω | τ(ω) < i} измеримо в F_i.

LaTeX

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

Lean4

protected theorem measurableSet_lt_of_countable_range (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable)
    (i : ι) : MeasurableSet[f i] {ω | τ ω < i} :=
  by
  have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by ext1 ω; simp [lt_iff_le_and_ne]
  rw [this]
  exact (hτ.measurableSet_le i).diff (hτ.measurableSet_eq_of_countable_range h_countable i)

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