neg_seq — Mathlib

English

The applicative product with a negated argument equals the negation of the product with the original argument: f <*> -x = -(f <*> x).

Русский

Умножение аппликативного типа на отрицательный аргумент равно отрицанию результата умножения на исходный аргумент: f <*> -x = -(f <*> x).

LaTeX

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

Lean4

@[simp]
theorem neg_seq (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : -f <*> x = -(f <*> x) :=
  neg_bind _ _

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