single_induction — Mathlib

English

The forward map sends a homomorphism φ to the family (φ ∘ mulSingle i).

Русский

Переходная функция отправляет гомоморфизм φ в семейство (φ ∘ mulSingle i).

LaTeX

$$$$ \\text{toFun}(\\phi) = (i \\mapsto \\phi \\circ \\mathrm{mulSingle}_i). $$$$

Lean4

theorem single_induction [AddCommMonoid M] (p : (ι → M) → Prop) (f : ι → M) (zero : p 0)
    (add : ∀ f g, p f → p g → p (f + g)) (single : ∀ i m, p (Pi.single i m)) : p f :=
  by
  cases nonempty_fintype ι
  rw [← Finset.univ_sum_single f]
  exact Finset.sum_induction _ _ add zero (by simp [single])

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