lawfulMonad — Mathlib

English

The Filter monad satisfies all the standard monad laws (identity and associativity).

Русский

Монада фильтров удовлетворяет всем стандартным законам монады (тождество и ассоциативность).

LaTeX

$$$ \text{LawfulMonad}(\text{Filter}) $$$

Lean4

protected theorem lawfulMonad : LawfulMonad Filter
    where
  map_const := rfl
  id_map _ := rfl
  seqLeft_eq _ _ := rfl
  seqRight_eq _ _ := rfl
  pure_seq _ _ := rfl
  bind_pure_comp _ _ := rfl
  bind_map _ _ := rfl
  pure_bind _ _ := rfl
  bind_assoc _ _ _ := rfl

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