measurableSet_le' — Mathlib

English

For a stopping time τ and any i, the set {ω : τ(ω) ≤ i} is measurable with respect to the stopping-time sigma-algebra.

Русский

Для остановочного времени τ множество {ω : τ(ω) ≤ i} является измеримым в отношении сигма-алгебры остановки.

LaTeX

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

Lean4

protected theorem measurableSet_le' (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ i} := by
  intro j
  have : {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω ≤ min i j} := by ext1 ω;
    simp only [Set.mem_inter_iff, Set.mem_setOf_eq, le_min_iff]
  rw [this]
  exact f.mono (min_le_right i j) _ (hτ _)

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