instBind

Mathlib.Order.Filter.Defs

URI: https://scilib.ai/kg/mathlib#Filter.instBind

English

There exists a Bind structure on the type of filters, with the bind operation given by Filter.bind.

Русский

Существует структура Bind над множеством фильтров, где операция bind задаётся через Filter.bind.

LaTeX

$$$\text{instance: } \mathrm{Bind}\ \mathrm{Filter}.$$$

Lean4

instance : Bind Filter :=
  ⟨@Filter.bind⟩

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

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

Разделы

Аффилиация

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