const_apply

Mathlib.Probability.Process.Filtration

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

English

The value of a constant filtration at index i is the constant σ-algebra m'.

Русский

Значение константной фильтрации в индексе i равно σ-алгебре m'.

LaTeX

$$$\\mathrm{const}(m',hm').seq(i) = m'$$$

Lean4

@[simp]
theorem const_apply {m' : MeasurableSpace Ω} {hm' : m' ≤ m} (i : ι) : const ι m' hm' i = m' :=
  rfl

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

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

Разделы

Аффилиация

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