prod_mul_tprod_subtype_compl — Mathlib

English

For any Multipliable f and finite s, the finite product over s times the tail tprod over the complement equals the total infinite product.

Русский

Для суммируемой f и конечного множества s произведение по s, умноженное на бесконечное произведение по дополнению, равно общему бесконечному произведению.

LaTeX

$$$$\\left(\\prod_{x\\in s} f(x)\\right) \\cdot \\prod' x : \\{ x \\notin s \\}, f x = \\prod' x, f x.$$$$

Lean4

@[to_additive]
protected theorem prod_mul_tprod_subtype_compl [T2Space α] {f : β → α} (hf : Multipliable f) (s : Finset β) :
    (∏ x ∈ s, f x) * ∏' x : { x // x ∉ s }, f x = ∏' x, f x :=
  by
  rw [← hf.tprod_subtype_mul_tprod_subtype_compl s]
  simp only [Finset.tprod_subtype', mul_right_inj]
  rfl

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