English
Let P be a property of finsupp functions f : ι →₀ M. If P(0) holds, if P is closed under addition (P f → P g → P(f + g)), and if P holds for every singleton (P(single a b) for all a,b), then P holds for all f.
Русский
Пусть P — свойство функции с конечной опорой f : ι →₀ M. Если P(0) верно, если P сохраняется под сложением (P f → P g → P(f + g)), и если P верно для каждого одинокого тождества (P(single a b) для любых a, b), тогда P верно для всей f.
LaTeX
$$$P(0) \to \left( \forall f,g:\iota \to_0 M,\ P(f) \to P(g) \to P(f+g) \right) \to \left( \forall a:\iota, \forall b:\,M,\ P(\mathrm{single}(a,b)) \right) \to \forall f:\iota \to_0 M,\ P(f).$$$
Lean4
@[elab_as_elim]
theorem induction_linear {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
(add : ∀ f g : ι →₀ M, motive f → motive g → motive (f + g)) (single : ∀ a b, motive (single a b)) : motive f :=
induction₂ f zero fun _a _b _f _ _ w => add _ _ w (single _ _)
