finprod_subtype_eq_finprod_cond — Mathlib

English

For any predicate p, the finprod over the subtype {x : α // p x} equals the finprod over {x : α | p x} with the same f.

Русский

Для любого p верно: произведение по подтипу {x | p x} равно произведению по множеству {x | p x} с той же функцией f.

LaTeX

$$$\\prod^\\!j : \\{x \\mid p(x)\\}, f(j) = \\prod^\\!i: \\{x \\mid p(x)\\}, f(i)$$$

Lean4

@[to_additive]
theorem finprod_subtype_eq_finprod_cond (p : α → Prop) : ∏ᶠ j : Subtype p, f j = ∏ᶠ (i) (_ : p i), f i :=
  finprod_set_coe_eq_finprod_mem {i | p i}

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