finsetProd — Mathlib

English

If f_i ~_l g_i for all i in a finite set s, then the product over i in s of f_i is equivalent to the product of g_i.

Русский

Если для всех i в конечном множестве s f_i ~_l g_i, то произведение по i ∈ s f_i эквивалентно произведению g_i.

LaTeX

$$$ \\forall i \\in s,\\ f_i \\sim_{l} g_i \\Rightarrow \\prod_{i \\in s} f_i(\\cdot) \\sim_{l} \\prod_{i \\in s} g_i(\\cdot) $$$

Lean4

theorem finsetProd {s : Finset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
    (∏ i ∈ s, f i ·) ~[l] (∏ i ∈ s, g i ·) :=
  multisetProd h

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