add_seq — Mathlib

English

Addition distributes inside the applicative: f + g <*> x = (f <*> x) + (g <*> x).

Русский

Сложение распределяется внутри аппликативного применения: f + g <*> x = (f <*> x) + (g <*> x).

LaTeX

$$$ \forall {\alpha \beta} (f g : FreeAbelianGroup(\alpha \to \beta)) (x : FreeAbelianGroup(\alpha)),\; f + g <*> x = (f <*> x) + (g <*> x)$$$

Lean4

@[simp]
theorem add_seq (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : f + g <*> x = (f <*> x) + (g <*> x) :=
  add_bind _ _ _

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