measurableSpace_le_of_le_const — Mathlib

English

If τ ω ≤ i for all ω, then hτ.measurableSpace ≤ f seq i.

Русский

Если для всех ω верно τ(ω) ≤ i, тогда hτ.measurableSpace ⊆ f_i.

LaTeX

$$$(\forall \omega,\ \tau(\omega) \le i) \Rightarrow h_{\tau}.\mathrm{measurableSpace} \le f_i$$$

Lean4

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

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