le_measurableSpace_of_const_le — Mathlib

English

Let hτ be a stopping time for a filtration f. If i is a fixed index with i ≤ τ(ω) for all ω, then the i-th sigma-algebra is contained in the stopping-time sigma-algebra.

Русский

Пусть hτ – остановочное время для фильтрации f. Если фиксированное число i не превосходит τ(ω) для всех ω, то σ-алгебра на уровне i вложена в σ-алгебру остановки.

LaTeX

$$$\forall i\; f(i) \le h_τ.m \quad\Rightarrow\quad f(i) \le h_τ.measurableSpace$$$

Lean4

theorem le_measurableSpace_of_const_le (hτ : IsStoppingTime f τ) {i : ι} (hτ_le : ∀ ω, i ≤ τ ω) :
    f i ≤ hτ.measurableSpace :=
  (measurableSpace_const _ _).symm.le.trans (measurableSpace_mono _ hτ hτ_le)

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