English
Let P be a property of finsupp functions f : ι →₀ M. If P(0) holds and, for all a,b,f, P(f) implies P(f + single a b) under a suitable order condition on the support, then P holds for all f.
Русский
Пусть P — свойство функции с конечной опорой. Если P(0) истинно и при любом a,b,f, P(f) ⇒ P(f + single a b) при условии порядка по опорному множеству, тогда P верно для всех f.
LaTeX
$$$P(0) \to \left( \forall a:\iota, \forall b:\,M, \forall f:\iota \to_0 M,\ (\forall c \in \operatorname{supp}(f), c < a) \to \, P(f) \to P(f + \mathrm{single}(a,b)) \right) \to \forall f:\iota \to_0 M,\ P(f).$$$
Lean4
/-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℤ` is not distributive
unless `F i`'s addition is commutative. -/
instance instIntSMul : SMul ℤ (ι →₀ G) :=
⟨fun n v => v.mapRange (n • ·) (zsmul_zero _)⟩
