measurableSet_gt' — Mathlib

English

For a stopping time hτ, the set {ω : i < τ(ω)} is measurable as well, i.e., a GT' result.

Русский

Для остановочного времени свойства множество {ω : i < τ(ω)} также измеримо.

LaTeX

$$$\{ω : i < τ(ω)\}$ is measurable in $h_τ.measurableSpace$.$$

Lean4

protected theorem measurableSet_gt' (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | i < τ ω} :=
  by
  have : {ω : Ω | i < τ ω} = {ω : Ω | τ ω ≤ i}ᶜ := by ext1 ω; simp
  rw [this]
  exact (hτ.measurableSet_le' i).compl

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