English
Let P be a property of finsupp functions f : ι →₀ M. If P(0) holds and for all a,b,f, whenever every c in the support of f is less than a for an order on ι, and b ≠ 0, P(f) implies P(instHAdd.hAdd f (single a b)), then P holds for all f.
Русский
Пусть P — свойство функции с конечной опорой f : ι →₀ M. Если P(0) истинно и для любых a,b,f, когда каждый элемент опоры f меньше a в заданном порядке ι, и b ≠ 0, из 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 b \neq 0 \to P(f) \to P(f + \mathrm{single}(a,b)) \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) (h0 : p 0)
(ha : ∀ (a b) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + single a b)) : p f :=
induction_on_max₂ (ι := ιᵒᵈ) f h0 ha
