measurableSet_eq' — Mathlib

English

If Topological/Order assumptions hold, for each i, the set {ω : τ(ω) = i} is measurable in the stopping-time sigma-algebra.

Русский

При соблюдении топологических условий множество {ω : τ(ω) = i} измеримо в сигма-алгебре остановки.

LaTeX

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

Lean4

protected theorem measurableSet_eq' [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
    (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[hτ.measurableSpace] {ω | τ ω = i} :=
  by
  rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]
  exact hτ.measurableSet_eq i

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