finprod_mem_congr — Mathlib

English

If s=t and f equals g on t, then the finprods over s and t coincide.

Русский

Если s=t и ∀x∈t, f(x)=g(x), то \$ \\prodᶠ i∈s f(i) = \\prodᶠ i∈t g(i) \$.

LaTeX

$$$\\displaystyle s=t \\Rightarrow (\\forall x\\in t, f(x)=g(x)) \\Rightarrow \\prod\\ᶠ i \\in s, f i = \\prod\\ᶠ i \\in t, g i$$$

Lean4

@[to_additive]
theorem finprod_mem_congr (h₀ : s = t) (h₁ : ∀ x ∈ t, f x = g x) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, g i :=
  h₀.symm ▸ finprod_congr fun i => finprod_congr_Prop rfl (h₁ i)

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