single_apply — Mathlib

English

The value of a basis element at a point is given by a conditional: (single a b) a' = b if a=a' and 0 otherwise.

Русский

Значение базисного элемента в точке равно b, если a=a', и 0 иначе.

LaTeX

$$$\\mathrm{single\\_apply}\\{a,a',b\\} : \\mathrm{single}\\ a\\ b\\ a' = \\text{if } a=a' \\text{ then } b \\text{ else } 0$$$

Lean4

@[to_additive]
theorem single_apply {a a' : M} {b : R} [Decidable (a = a')] : single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

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