measurable_of_le — Mathlib

English

If hτ is a stopping time with respect to f, then τ is measurable as a function into ι, in the ambient topological/measure structure.

Русский

Если hτ – остановочное время относительно фильтрации f, то τ — измерима как функция в целое ι.

LaTeX

$$$τ \text{ is measurable w.r.t. } h_τ.measurableSpace$$$

Lean4

protected theorem measurable_of_le [TopologicalSpace ι] [MeasurableSpace ι] [BorelSpace ι] [OrderTopology ι]
    [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) {i : ι} (hτ_le : ∀ ω, τ ω ≤ i) : Measurable[f i] τ :=
  hτ.measurable.mono (measurableSpace_le_of_le_const _ hτ_le) le_rfl

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