prod_mul_tprod_compl — Mathlib

English

For a finite set s, the product over s times the tail product over its complement equals the full tprod: (∏_{x∈s} f(x)) · ∏'_{x∈s^c} f(x) = ∏'_{x} f(x).

Русский

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

LaTeX

$$$\bigl(\prod_{x\in s} f(x)\bigr) \cdot \prod' x : (s)^c, f(x) = \prod' x, f(x).$$$

Lean4

@[to_additive]
protected theorem prod_mul_tprod_compl {s : Finset β} (hf : Multipliable f) :
    (∏ x ∈ s, f x) * ∏' x : ↑(s : Set β)ᶜ, f x = ∏' x, f x :=
  ((s.hasProd f).mul_compl (s.multipliable_compl_iff.2 hf).hasProd).tprod_eq.symm

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