piFinset_mul — Mathlib

English

For a finite index set ι and families of finite sets s_i, t_i, the product over i of (s_i · t_i) equals the product of the families: piFinset (i ↦ s_i · t_i) = piFinset s · piFinset t.

Русский

Для конечного множества индексов ι и семейств конечных множеств s_i и t_i выполняется равенство: piFinset (i ↦ s_i · t_i) = piFinset s · piFinset t.

LaTeX

$$$\pi\text{-Finset}(i \mapsto s_i \cdot t_i) = \pi\text{-Finset}(s) \cdot \pi\text{-Finset}(t)$$$

Lean4

@[to_additive]
theorem piFinset_mul [∀ i, Mul (α i)] (s t : ∀ i, Finset (α i)) :
    piFinset (fun i ↦ s i * t i) = piFinset s * piFinset t :=
  piFinset_image₂ _ _ _

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