instLawfulMonad — Mathlib

English

Set forms a lawful monad with the given definitions of bind, pure, and map obeying the usual monad laws.

Русский

Set образует законную монадy с данными определениями bind, pure и map, удовлетворяющими обычным монадным законам.

LaTeX

$$$\mathrm{LawfulMonad}(\mathrm{Set})$$$

Lean4

instance : LawfulMonad Set where
  bind_pure_comp _ _ := (image_eq_iUnion _ _).symm
  bind_map _ _ := seq_def.symm
  pure_bind := biUnion_singleton
  bind_assoc _ _ _ := by simp only [bind_def, biUnion_iUnion]

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