mono

Mathlib.Probability.Process.Filtration

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

English

Filtration is monotone: if i ≤ j then f i ≤ f j.

Русский

Фильтрация монотонна: если i ≤ j, то f i ≤ f j.

LaTeX

$$$\\forall\\{i\\,j: ι\\},\\ i \\le j \\Rightarrow f.i \\le f.j$$$

Lean4

protected theorem mono {i j : ι} (f : Filtration ι m) (hij : i ≤ j) : f i ≤ f j :=
  f.mono' hij

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

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

Разделы

Аффилиация

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