induction₂ — Mathlib

English

For any finite set s, and x,y defined on s, mk s (x + y) = mk s x + mk s y.

Русский

Для конечного множества s и функций x, y на s выполняется mk s (x + y) = mk s x + mk s y.

LaTeX

$$$ mk s (x + y) = mk s x + mk s y $$$

Lean4

theorem induction₂ {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i) (h0 : p 0)
    (ha : ∀ (i b) (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)) : p f :=
  DFinsupp.induction f h0 fun i b f h1 h2 h3 =>
    have h4 : f + single i b = single i b + f := by
      ext j; by_cases H : i = j
      · subst H
        simp [h1]
      · simp [H]
    Eq.recOn h4 <| ha i b f h1 h2 h3

Похожие утверждения