measurableSet_gt — Mathlib

English

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 < \tau(\omega)\} \in \mathcal{F}_i$$$

Lean4

theorem measurableSet_gt (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_le]
  rw [this]
  exact (hτ.measurableSet_le i).compl

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