prod_subtype — Mathlib

English

If p is a predicate on ι and the Finset s is such that x ∈ s ⇔ p x, then ∏ a ∈ s, f a = ∏ a : Subtype p, f a.

Русский

Если p — предикат на ι и Finset s удовлетворяет x ∈ s ⇔ p x, то произведение по s равно произведению по подтипу p: ∏ a ∈ s, f a = ∏ a : Subtype p, f a.

LaTeX

$$$\displaystyle \prod a ∈ s, f a = \prod a : Subtype p, f a$$$

Lean4

@[to_additive]
theorem prod_subtype {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι) (h : ∀ x, x ∈ s ↔ p x) (f : ι → M) :
    ∏ a ∈ s, f a = ∏ a : Subtype p, f a := by
  have : (· ∈ s) = p := Set.ext h
  subst p
  rw [← prod_coe_sort]
  congr!

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