prod_congr — Mathlib

English

If f and g are functions α → M with f(a) = g(a) for every a, then their products over α are equal.

Русский

Если f(a) = g(a) для каждого a, то произведения по a в α совпадают.

LaTeX

$$$\\prod_{a \\in \\mathrm{univ}} f(a) = \\prod_{a \\in \\mathrm{univ}} g(a)\\quad \\text{whenever } f(a)=g(a)\\text{ for all } a$$$

Lean4

@[to_additive]
theorem prod_congr (f g : α → M) (h : ∀ a, f a = g a) : ∏ a, f a = ∏ a, g a :=
  Finset.prod_congr rfl fun a _ha => h a

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