instLawfulMonad — Mathlib

English

The Finset instance forms a lawful monad: the monad laws (associativity of bind, left/right identity with pure) hold for Finset.

Русский

Экземпляр Finset образует законную монаду: законы монады (ассоциативность связывания, левый и правый тождественные элементы с pure) выполняются для Finset.

LaTeX

$$$$ \\text{Finset is a LawfulMonad.} $$$$

Lean4

instance : LawfulMonad Finset :=
  { Finset.lawfulApplicative with
    bind_pure_comp := fun _ _ => sup_singleton_apply _ _
    bind_map := fun _ _ => rfl
    pure_bind := fun _ _ => sup_singleton
    bind_assoc := fun s f g => by simp only [bind, sup_eq_biUnion, biUnion_biUnion] }

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