instTop

Mathlib.Probability.Process.Filtration

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

English

There is a top filtration given by a constant top element.

Русский

Существует верхняя фильтрация, заданная константной верхней границей.

LaTeX

$$$\\mathrm{Top}\\ (\\mathrm{Filtration}\\ ι\\ m) := \\mathrm{const}\\ ι\\ \\top\\;\\top\\_le$$$

Lean4

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

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

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

Разделы

Аффилиация

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