tprod_subtype — Mathlib

English

For any set s, the tprod over s equals the tprod over the subindicator: ∏' x : s, f x = ∏' x, s.mulIndicator f x.

Русский

Для множества s т-произведение по s равно т-произведению по индикатору множества s.

LaTeX

$$$\\\\prod' x : s, f x = \\\\prod' x, s.mulIndicator f x$$$

Lean4

@[to_additive]
theorem tprod_subtype (s : Set β) (f : β → α) : ∏' x : s, f x = ∏' x, s.mulIndicator f x :=
  by
  rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]
  simp

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