instInhabited

Mathlib.Probability.Process.Filtration

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Filtration.instInhabited

English

Specialization of progMeasurable_of_tendsto' to ℕ-indexed processes with atTop tending to u.

Русский

Специализация progMeasurable_of_tendsto' на процессы с индексами ℕ, сходящиеся к u.

LaTeX

$${\\forall l, \\mathrm{ProgMeasurable}(f, U l) } \\Rightarrow \\mathrm{Tendsto} U\\ fltr (nhds\\ u) \\Rightarrow \\mathrm{ProgMeasurable}(f, u)$$

Lean4

instance : Inhabited (Filtration ι m) :=
  ⟨const ι m le_rfl⟩

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

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

Разделы

Аффилиация

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