measurableSet_ge — Mathlib

English

For any i, the set {ω ∈ Ω : i ≤ τ(ω)} is measurable in F_i.

Русский

Для любого i множество {ω ∈ Ω : i ≤ τ(ω)} измеримо относительно F_i.

LaTeX

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

Lean4

theorem measurableSet_ge (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[f i] {ω | i ≤ τ ω} :=
  by
  have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]
  rw [this]
  exact (hτ.measurableSet_lt i).compl

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