map_neg — Mathlib

English

For any f : α → β and x ∈ FreeAbelianGroup α, map f of -x equals - map f x.

Русский

Для любой f : α → β и x ∈ FreeAbelianGroup α отображение f к -x равно -(отображение f к x).

LaTeX

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

Lean4

@[simp]
protected theorem map_neg (f : α → β) (x : FreeAbelianGroup α) : f <$> (-x) = -f <$> x :=
  map_neg (lift <| of ∘ f) _

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