SetM

Mathlib.Data.Set.Functor

URI: https://scilib.ai/kg/mathlib#SetM

English

The SetM construction carries a lawful monad structure, i.e., it satisfies the monad laws with its unit and multiplication.

Русский

У конструкции SetM имеется законная монада: она удовлетворяет мона́дным законам с единицей и умножением.

LaTeX

$$$\mathrm{LawfulMonad}(\mathrm{SetM}).$$$

Lean4

/-- This is `Set` but with a `Monad` instance. -/
def SetM (α : Type u) :=
  Set α

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

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

Разделы

Аффилиация

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