English
Let P be a property of finsupp functions f : ι →₀ M. If P(0) holds and, for any a,b and f, whenever every element in the support of f is strictly less 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), c < a) \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 increasing `a`.
The lemma `induction_on_max₂` swaps the argument order in the sum. -/
theorem induction_on_max (f : ι →₀ M) (zero : p 0)
(single_add : ∀ a b (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (single a b + f)) : p f :=
by
suffices ∀ (s) (f : ι →₀ M), f.support = s → p f from this _ _ rfl
refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
· rwa [support_eq_empty.1 h]
· have hs' : (erase a f).support = s := by rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
rw [← single_add_erase a f]
refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
rw [← mem_support_iff, hs]
exact mem_insert_self a s
