mapRange_add' — Mathlib

English

Under FunLike and AddMonoidHomClass assumptions, mapRange preserves addition for FinSupps in a primed form.

Русский

При соответствующих предположениях FunLike и AddMonoidHomClass mapRange сохраняет сложение для FinSupp в упрощённой форме.

LaTeX

$$$\\text{mapRange } f (\\mathbf{g}_1 + \\mathbf{g}_2) = \\text{mapRange } f \\mathbf{g}_1 + \\text{mapRange } f \\mathbf{g}_2$$$

Lean4

theorem mapRange_add' [FunLike F M N] [AddMonoidHomClass F M N] {f : F} (g₁ g₂ : ι →₀ M) :
    mapRange f (map_zero f) (g₁ + g₂) = mapRange f (map_zero f) g₁ + mapRange f (map_zero f) g₂ :=
  mapRange_add (map_add f) g₁ g₂

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