sub_seq — Mathlib

English

The difference distributes through the applicative: f - g <*> x = (f <*> x) - (g <*> x).

Русский

Разность распределяется через аппликативное применениe: 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 sub_seq (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : f - g <*> x = (f <*> x) - (g <*> x) :=
  sub_bind _ _ _

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