prod_mulIndicator_eq_prod_inter — Mathlib

English

The product over s of (t i).mulIndicator f i equals the product over i ∈ s∩t of f i.

Русский

Произведение по i∈s of (t i).mulIndicator f i равно произведению по i в пересечении s и t.

LaTeX

$$$\prod i \in s, (t(i).mulIndicator f(i)) = \prod i \in s \cap t, f(i)$$$

Lean4

@[to_additive]
theorem prod_mulIndicator_eq_prod_inter [DecidableEq ι] (s t : Finset ι) (f : ι → β) :
    ∏ i ∈ s, (t : Set ι).mulIndicator f i = ∏ i ∈ s ∩ t, f i := by
  rw [← filter_mem_eq_inter, prod_mulIndicator_eq_prod_filter]; rfl

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