prod_union_inter — Mathlib

English

For any finite sets s1 and s2, the product over their union times the product over their intersection equals the product over s1 times the product over s2.

Русский

Для двух конечных множеств s1 и s2 произведение по их объединению, умноженное на произведение по их пересечению, равно произведению по s1 и по s2.

LaTeX

$$$\\left(\\prod_{x\\in s_1 \\cup s_2} f(x)\\right) \\left(\\prod_{x\\in s_1 \\cap s_2} f(x)\\right) = \\left(\\prod_{x\\in s_1} f(x)\\right) \\left(\\prod_{x\\in s_2} f(x)\\right)$$$

Lean4

@[to_additive]
theorem prod_union_inter [DecidableEq ι] :
    (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x :=
  fold_union_inter

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