prod_subtypeDomain_index — Mathlib

English

If hp holds for all x in the support of v, then the product over the subtypeDomain equals the product over v.

Русский

Если hp выполняется для каждого x в опоре v, то произведение над подтип-доменом равно произведению над v.

LaTeX

$$$$ (v.subtypeDomain p).\\mathrm{prod} (\\lambda a b, h\\,a b) = v.\\mathrm{prod} h. $$$$

Lean4

@[to_additive]
theorem prod_subtypeDomain_index [CommMonoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ x ∈ v.support, p x) :
    (v.subtypeDomain p).prod (fun a b ↦ h a b) = v.prod h := by
  refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop

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