measurableSet_lt_le

Mathlib.Probability.Process.Stopping

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsStoppingTime.measurableSet_lt_le

← MathLib Explorer

English

If i ≤ j, then {ω ∈ Ω : τ(ω) < i} is measurable in F_j.

Русский

Если i ≤ j, то {ω ∈ Ω : τ(ω) < i} измеримо относительно F_j.

LaTeX

$$$\forall i,j,\ i \le j \Rightarrow \{\omega \in \Omega \mid \tau(\omega) < i\} \in \mathcal{F}_j$$$

Lean4

theorem measurableSet_lt_le (hτ : IsStoppingTime f τ) {i j : ι} (hle : i ≤ j) : MeasurableSet[f j] {ω | τ ω < i} :=
  f.mono hle _ <| hτ.measurableSet_lt i

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru