measurableSet_lt' — Mathlib

English

The set {ω : τ(ω) < i} is measurable under a stopping-time sigma-algebra, given appropriate structure.

Русский

Множество {ω : τ(ω) < i} измеримо в сигма-алгебре остановки.

LaTeX

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

Lean4

protected theorem measurableSet_lt' [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
    (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[hτ.measurableSpace] {ω | τ ω < i} :=
  by
  have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} :=
    by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]
  rw [this]
  exact (hτ.measurableSet_le' i).diff (hτ.measurableSet_eq' i)

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