mapRange_neg' — Mathlib

English

A variant of mapRange negation: mapRange f (map_zero f) (-v) = - mapRange f (map_zero f) v.

Русский

Вариант негативности mapRange: mapRange f (map_zero f) (-v) = - mapRange f (map_zero f) v.

LaTeX

$$$\forall v:\ ι \to_{0} G:\ mapRange\ f\ (map\_zero\ f)\ (-v) = - mapRange\ f\ (map\_zero\ f)\ v$$$

Lean4

theorem mapRange_neg' [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (v : ι →₀ G) :
    mapRange f (map_zero f) (-v) = -mapRange f (map_zero f) v :=
  mapRange_neg (map_neg f) v

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