finprod_mem_univ — Mathlib

English

The finprod over the universal set equals the finprod over all indices.

Русский

Произведение по всеиндексационному множеству эквивалентно произведению по всем индексам.

LaTeX

$$$\\displaystyle \\prod\\ᶠ i \\in Univ,\\ f(i) = \\prod\\ᶠ i:\\n α,\\ f(i)$$$

Lean4

@[to_additive]
theorem finprod_mem_univ (f : α → M) : ∏ᶠ i ∈ @Set.univ α, f i = ∏ᶠ i : α, f i :=
  finprod_congr fun _ => finprod_true _

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