instCommApplicative — Mathlib

English

The Filter functor with map and product is a commutative applicative; the order of applying effects via the product operation does not matter.

Русский

Функтор Filter с map и произведением обладает коммутативной аппликативностью; порядок применения эффектов через операцию произведения неважен.

LaTeX

$$$\\text{Filter with }\\mathrm{map}\\text{ and }\\mathrm{prod}\\text{ is a commutative applicative}.$$

Lean4

instance : CommApplicative (Filter : Type u → Type u) :=
  ⟨fun f g => prod_map_seq_comm f g⟩

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