English
Let P be a property of finitely supported functions f : ι →₀ M. If P(0) holds and, for all a,b with b ≠ 0 and all f, a ∉ supp f implies P(f) → P(f + single a b), then P holds for every f.
Русский
Пусть P — свойство функции с конечной опорой f : ι →₀ M. Если P(0) верно и для любых a, b с b ≠ 0 и любого f, где a не принадлежит опоре f, из 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,\ a \notin \operatorname{supp}(f) \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
@[elab_as_elim]
theorem induction₂ {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
(add_single : ∀ (a b) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)) : motive f := by
classical
refine f.induction zero ?_
convert add_single using 7
apply (addCommute_of_disjoint _).eq
simp_all [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem, single_apply]
