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 satisfies a certain order condition up to a, and b ≠ 0, P(f) implies P(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 : \iota, c \in \operatorname{supp}(f) \to \ ) \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 increasing `a`.
The lemma `induction_on_max` swaps the argument order in the sum. -/
theorem induction_on_max₂ (f : ι →₀ M) (zero : p 0)
(add_single : ∀ a b (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) : p f := by
classical
refine f.induction_on_max zero ?_
convert add_single using 7 with _ _ _ H
have := fun c hc ↦ (H c hc).ne
apply (addCommute_of_disjoint _).eq
simp_all [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem, single_apply, not_imp_not]
