English
Let motive be a property of elements of the direct sum. If motive holds for zero, holds on every pure element of the form of i x, and is closed under addition, then motive holds for every element.
Русский
Пусть свойство motive относится к элементам прямой суммы. Если motive верно для нуля, верно для каждого элемента вида of i x, и сохраняется при сложении, тогда motive верно для каждого элемента.
LaTeX
$$$\forall \text{motive} : (DirectSum ι \ β i) \to \mathrm{Prop},\ motive\ 0\ \wedge\ (\forall i\ (x:\β i),\ motive(\mathrm{of}\ β i x))\ \wedge\ (\forall x y,\ motive x\to motive y\to motive(x+y))\ \Rightarrow\ (\forall x,\ motive x)$$$
Lean4
@[elab_as_elim]
protected theorem induction_on {motive : (⨁ i, β i) → Prop} (x : ⨁ i, β i) (zero : motive 0)
(of : ∀ (i : ι) (x : β i), motive (of β i x)) (add : ∀ x y, motive x → motive y → motive (x + y)) : motive x :=
by
apply DFinsupp.induction x zero
intro i b f h1 h2 ih
solve_by_elim
