coe_add — Mathlib

English

For any two locally finitely supported Y-valued functions D1 and D2, the function obtained by adding them and then viewing as a function equals the pointwise sum of their underlying functions.

Русский

Для двух функций с локально конечной поддержкой в Y, сумма функций, представленная как функция, равна точечной сумме их значений.

LaTeX

$$$((D_1 + D_2) : X \\to Y) = (D_1 : X \\to Y) + (D_2 : X \\to Y)$$$

Lean4

@[simp]
theorem coe_add [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) : (↑(D₁ + D₂) : X → Y) = D₁ + D₂ :=
  rfl

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