English
If e is a FunLike map with a zero-preserving property, then e applied to the finitely supported function that is m at index i equals the finitely supported function that has e(m) at i. In symbols, e(single i m)(b) = (single i (e m))(b) for all i, m, b.
Русский
Если e является отображением, сохраняющим нулевое, то применение e к функциgии с единичной опорой в i даёт функцию с значением e(m) в i. В символах: e(single i m)(b) = (single i (e m))(b) для всех i, m, b.
LaTeX
$$$e(\\text{single}_i m)(b) = (\\text{single}_i (e m))(b)$$$
Lean4
theorem apply_single [FunLike F M N] [ZeroHomClass F M N] (e : F) (i : ι) (m : M) (b : ι) :
e (single i m b) = single i (e m) b :=
apply_single' e (map_zero e) i m b
