monad

Mathlib.Order.Filter.Map

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

English

The collection of filters carries a Monad structure, with map given by Filter.map.

Русский

Множество фильтров обладает структурой монад, причём отображение задаётся через Filter.map.

LaTeX

$$$ \text{Monad}(\text{Filter}) \text{ with } \mathrm{map} = \mathrm{Filter.map}. $$$

Lean4

/-- The monad structure on filters. -/
protected def monad : Monad Filter where map := @Filter.map

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

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

Разделы

Аффилиация

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