mapRange_neg — Mathlib

English

If f respects negation (hf'), then mapRange preserves negation: mapRange f hf (-v) = - mapRange f hf v.

Русский

Если f удовлетворяет условию сохранения отрицания, то mapRange сохраняет отрицание: mapRange f hf (-v) = - mapRange f hf v.

LaTeX

$$$\forall v,\ mapRange\ f\ hf\ (-v) = -\ mapRange\ f\ hf\ v$$$

Lean4

theorem mapRange_neg [NegZeroClass G] [NegZeroClass H] {f : G → H} {hf : f 0 = 0} (hf' : ∀ x, f (-x) = -f x)
    (v : ι →₀ G) : mapRange f hf (-v) = -mapRange f hf v :=
  ext fun _ => by simp only [hf', neg_apply, mapRange_apply]

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