prod_of_support_subset — Mathlib

English

Let f: α →₀ M be a finitely supported function and s a Finset with supp f ⊆ s. For any g: α → M → N and h: ∀ i ∈ s, g i 0 = 1, we have f.prod g = ∏ x ∈ s, g x (f x).

Русский

Пусть f: α →₀ M имеет конечную опору и s — Finset с supp f ⊆ s. Тогда для любого g: α → M → N и h: ∀ i ∈ s, g i 0 = 1, выполняется f.prod g = ∏ x ∈ s, g x (f x).

LaTeX

$$$ f \\in α \\to₀ M, \\\\text{supp } f ⊆ s \\\\Rightarrow f.prod g = \\\\prod_{x \\in s} g x (f x) $$$

Lean4

@[to_additive]
theorem prod_of_support_subset (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N)
    (h : ∀ i ∈ s, g i 0 = 1) : f.prod g = ∏ x ∈ s, g x (f x) :=
  by
  refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)
  exact notMem_support_iff.1 hx

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