English
Let P be a property of finsupp functions f : ι →₀ M. If P(0) and, for all a,b,f, whenever every element of the support of f is strictly greater than a, and b ≠ 0, P(f) implies P(single a b + f), then P holds for all f.
Русский
Пусть P — свойство функции с конечной опорой f : ι →₀ M. Если P(0) и для любых a,b,f, когда каждый элемент опоры f строго больше a, и b ≠ 0, из P(f) следует P(single a b + f), тогда 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), a < c) \to b \neq 0 \to P(f) \to P(\mathrm{single}(a,b) + f) \right) \to \forall f:\iota \to_0 M,\ P(f).$$$
Lean4
/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.
The lemma `induction_on_min₂` swaps the argument order in the sum. -/
theorem induction_on_min (f : ι →₀ M) (zero : p 0)
(single_add : ∀ a b (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (single a b + f)) : p f :=
induction_on_max (ι := ιᵒᵈ) f zero single_add
