English
Let P be a property of finitely supported functions f : ι →₀ M. If P holds for the zero function and if, whenever a ∈ ι, b ∈ M with b ≠ 0, and f is a finitely supported function with a not in its support, P(f) implies P(single a b + f), then P holds for every finitely supported function.
Русский
Пусть P — свойство функций с конечной опорой f : ι →₀ M. Если P верно для нулевой функции и если для любых a ∈ ι, b ∈ M с b ≠ 0, и f с a ∉ supp f выполняется P(f) ⇒ P(single a b + f), то P верно для всякой функции с конечной опорой.
LaTeX
$$$P(0) \to \left( \forall a:\iota\,\forall b: M\,\forall f: \iota \to_0 M,\ a \notin \operatorname{supp}(f) \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
@[elab_as_elim]
protected theorem induction {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
(single_add : ∀ (a b) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)) : motive f :=
suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
fun s =>
Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf =>
by
suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this
classical
apply single_add
· rw [support_erase, mem_erase]
exact fun H => H.1 rfl
· rw [← mem_support_iff, hf]
exact mem_cons_self _ _
· apply ih _ _
rw [support_erase, hf, Finset.erase_cons]
