prod_subtypeDomain_index — Mathlib

English

If v is a DFinsupp and p a predicate, then the product over the subtype domain equals the product over the original domain, provided hp holds for all elements in v.

Русский

Если v — DFinsupp и p — предикат, то произведение по подтипу равно произведению по исходному диапазону, при условии hp.

LaTeX

$$$ (v.subtypeDomain p).prod (\\lambda i, b. h(i,b)) = v.prod (\\lambda i, b. h(i,b)). $$$

Lean4

@[to_additive]
theorem prod_subtypeDomain_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {v : Π₀ i, β i}
    {p : ι → Prop} [DecidablePred p] {h : ∀ i, β i → γ} (hp : ∀ x ∈ v.support, p x) :
    (v.subtypeDomain p).prod (fun i b => h i b) = v.prod h := by
  refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop

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