prod_mulIndicator_subset — Mathlib

English

For f: ι → β and s ⊆ t, the product over t of mulIndicator (↑s) f i equals the product over s of f i.

Русский

Для f: ι → β и s ⊆ t верно: ∏ i∈t mulIndicator(↑s) f i = ∏ i∈s f i.

LaTeX

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

Lean4

/-- Taking the product of an indicator function over a possibly larger finset is the same as
taking the original function over the original finset. -/
@[to_additive /-- Summing an indicator function over a possibly larger `Finset` is the same as
    summing the original function over the original finset. -/
    ]
theorem prod_mulIndicator_subset (f : ι → β) {s t : Finset ι} (h : s ⊆ t) :
    ∏ i ∈ t, mulIndicator (↑s) f i = ∏ i ∈ s, f i :=
  prod_mulIndicator_subset_of_eq_one _ (fun _ ↦ id) h fun _ ↦ rfl

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