English
A variant of induction over a direct sum uses the lof map to build the result from zeros, individual components, and sums.
Русский
Вариант индукции по прямому сумме использует отображение lof для построения результата из нулей, отдельных компонент и сумм.
LaTeX
$$$\\text{induction\_lon }(R, \\iota, M, x) = \\dots$$$
Lean4
/-- A variant of `DirectSum.induction_on` that uses `DirectSum.lof` instead of `.of` -/
theorem induction_lon {R : Type*} [Semiring R] {ι : Type*} [DecidableEq ι] {M : ι → Type*}
[(i : ι) → AddCommMonoid <| M i] [(i : ι) → Module R (M i)] {motive : (⨁ i, M i) → Prop} (x : ⨁ i, M i)
(zero : motive 0) (lof : ∀ i (x : M i), motive (lof R ι M i x))
(add : ∀ (x y : ⨁ i, M i), motive x → motive y → motive (x + y)) : motive x := by
induction x using DirectSum.induction_on with
| zero => exact zero
| of => exact lof _ _
| add x y hx hy => exact add x y hx hy
