finprod_congr_Prop — Mathlib

English

If p = q and f,g are related by f(h) = g(h) for all h ∈ q, then finprod f = finprod g.

Русский

Если p = q и для всех h ∈ q выполняется f(h) = g(h), тогда finprod f = finprod g.

LaTeX

$$$\\mathrm{finprod\\_congr\\_Prop} : (p=q) \\Rightarrow (\\forall h:\\, q, f(h) = g(h)) \\Rightarrow \\mathrm{finprod}(f) = \\mathrm{finprod}(g)$$$

Lean4

@[to_additive (attr := congr)]
theorem finprod_congr_Prop {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q) (hfg : ∀ h : q, f (hpq.mpr h) = g h) :
    finprod f = finprod g := by
  subst q
  exact finprod_congr hfg

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