measurableSpace_le_of_le — Mathlib

English

Let f be a filtration on Ω with IsStoppingTime τ. If there exists an upper bound n such that τ(ω) ≤ n for all ω, then the stopping-time sigma-algebra generated by τ is contained in the ambient sigma-algebra m.

Русский

Пусть задана фильтрация f на Ω и остановочное время τ. Если существует верхняя граница n такая, что τ(ω) ≤ n для всех ω, то σ-алгебра остановки τ вложена в данную сигма-алгебру m.

LaTeX

$$$\text{If } h_\tau \text{ is a stopping time and } (∀\,\omega)\; τ(\omega) \le n, \text{ then } h_\tau.{\text{measurableSpace}} \le m.$$$

Lean4

theorem measurableSpace_le_of_le (hτ : IsStoppingTime f τ) {n : ι} (hτ_le : ∀ ω, τ ω ≤ n) : hτ.measurableSpace ≤ m :=
  (hτ.measurableSpace_le_of_le_const hτ_le).trans (f.le n)

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