mapRange_add — Mathlib

English

If f preserves zero and is additive, then mapRange of f distributes over the addition of finsupps: mapRange f (v1 + v2) = mapRange f v1 + mapRange f v2.

Русский

Если f сохраняет ноль и аддитивен, то mapRange распределяется по сложению FinSupp: mapRange f (v1+v2) = mapRange f v1 + mapRange f v2.

LaTeX

$$$\\text{mapRange } f \\; hf\\; (v_1 + v_2) = \\text{mapRange } f \\; hf\\; v_1 + \\text{mapRange } f \\; hf\\; v_2$$$

Lean4

theorem mapRange_add {hf : f 0 = 0} (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : ι →₀ M) :
    mapRange f hf (v₁ + v₂) = mapRange f hf v₁ + mapRange f hf v₂ :=
  ext fun _ => by simp only [hf', add_apply, mapRange_apply]

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