measurable — Mathlib

English

The set {ω : min(τ(ω), i) ≤ i} is measurable in the min sigma-algebra.

Русский

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

LaTeX

$$$\{ω : \min(τ(ω), i) \le i\}$ measurable in the min_sigma-algebra.$$

Lean4

protected theorem measurable [TopologicalSpace ι] [MeasurableSpace ι] [BorelSpace ι] [OrderTopology ι]
    [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) : Measurable[hτ.measurableSpace] τ :=
  @measurable_of_Iic ι Ω _ _ _ hτ.measurableSpace _ _ _ _ fun i => hτ.measurableSet_le' i

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