tsub — Mathlib

English

There is a natural truncated subtraction on the space DFinsupp Π₀ i, α_i, defined coordinatewise by (f - g)(i) = f(i) - g(i).

Русский

На пространстве DFinsupp Π₀ i, α_i имеется естественная усечённая вычитание, задаваемое по координатам: (f − g)(i) = f(i) − g(i).

LaTeX

$$$ \forall i,\ (f - g)(i) = f(i) - g(i) $$$

Lean4

/-- This is called `tsub` for truncated subtraction, to distinguish it with subtraction in an
additive group. -/
instance tsub : Sub (Π₀ i, α i) :=
  ⟨zipWith (fun _ m n ↦ m - n) fun _ ↦ tsub_self 0⟩

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