mulSingle_induction — Mathlib

English

The inverse maps a family (ψ_i) to the product ∏_i ψ_i ∘ eval_i.

Русский

Обратная карта берет семейство (ψ_i) и строит произведение по i: ∏_i ψ_i ∘ eval_i.

LaTeX

$$$$ \\text{invFun}(\\psi) = \\prod_{i\\in I} (\\psi_i \\circ \\mathrm{eval}_i). $$$$

Lean4

@[to_additive existing (attr := elab_as_elim)]
theorem mulSingle_induction [CommMonoid M] (p : (ι → M) → Prop) (f : ι → M) (one : p 1)
    (mul : ∀ f g, p f → p g → p (f * g)) (mulSingle : ∀ i m, p (Pi.mulSingle i m)) : p f :=
  by
  cases nonempty_fintype ι
  rw [← Finset.univ_prod_mulSingle f]
  exact Finset.prod_induction _ _ mul one (by simp [mulSingle])

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