measurableSet_ge' — Mathlib

English

For a stopping time τ, the set {ω : i ≤ τ(ω)} is measurable (under suitable topology/structure).

Русский

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

LaTeX

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

Lean4

protected theorem measurableSet_ge' [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
    (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[hτ.measurableSpace] {ω | i ≤ τ ω} :=
  by
  have : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω} :=
    by
    ext1 ω
    simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
    rw [@eq_comm _ i, or_comm]
  rw [this]
  exact (hτ.measurableSet_eq' i).union (hτ.measurableSet_gt' i)

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