measurableSet — Mathlib

English

The main property of the stopping-time associated measurable space is that a set s is measurable iff all intersections s ∩ {τ ≤ i} are measurable in F_i.

Русский

Основное свойство связанной сигма‑алгебры остановочного времени: множество s измеримо тогда и только тогда, когда все пересечения s ∩ {τ ≤ i} измеримы в F_i.

LaTeX

$$$\text{MeasurableSet}_{τ}(s) \iff \forall i,\text{MeasurableSet}[\mathcal{F}_i](s \cap \{\omega: τ(\omega) ≤ i\})$$$

Lean4

protected theorem measurableSet (hτ : IsStoppingTime f τ) (s : Set Ω) :
    MeasurableSet[hτ.measurableSpace] s ↔ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) :=
  Iff.rfl

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