instLE

Mathlib.Probability.Process.Filtration

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

English

There is a canonical lattice order on filtrations given pointwise by i: f i ≤ g i.

Русский

Существует каноническое частично-порядковое отношение на фильтрациях: f i ≤ g i по каждому i.

LaTeX

$$$\\mathrm{instLE}.le\\ (f,g) := \\forall i, f.i \\le g.i$$$

Lean4

instance : LE (Filtration ι m) :=
  ⟨fun f g => ∀ i, f i ≤ g i⟩

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

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

Разделы

Аффилиация

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