coe_sub — Mathlib

English

For locally finitely supported Y-valued functions D1 and D2, the difference D1 − D2 corresponds to the pointwise difference of their representing functions.

Русский

Разность двух функций с локально конечной поддержкой соответствует точечной разности их значений.

LaTeX

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

Lean4

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

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