mulIndicator_prod — Mathlib

English

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

Русский

Произведение mulIndicator над t от ∏ f(i) равно ∏ mulIndicator t(f(i)).

LaTeX

$$$\operatorname{mulIndicator} t\left(\prod i \in s, f(i)\right) = \prod i \in s, \operatorname{mulIndicator} t(f(i))$$$

Lean4

@[to_additive]
theorem mulIndicator_prod (s : Finset ι) (t : Set κ) (f : ι → κ → β) :
    mulIndicator t (∏ i ∈ s, f i) = ∏ i ∈ s, mulIndicator t (f i) :=
  map_prod (mulIndicatorHom _ _) _ _

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