instLawfulMonadSetM

Mathlib.Data.Set.Functor

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

English

SetM forms a lawful monad; the monad laws hold for SetM.

Русский

SetM образует законную монаду; выполняются все законы монады.

LaTeX

$$$$ \\operatorname{LawfulMonad}(SetM) $$$$

Lean4

instance : LawfulMonad SetM :=
  Set.instLawfulMonad

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

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

Разделы

Аффилиация

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