prod_union — Mathlib

English

If s1 and s2 are disjoint, then the product over their union equals the product over s1 times the product over s2.

Русский

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

LaTeX

$$$\\text{Disjoint}(s_1,s_2) \\Rightarrow \\prod_{x \\in s_1 \\cup s_2} f(x) = \\left(\\prod_{x \\in s_1} f(x)\\right) \\left(\\prod_{x \\in s_2} f(x)\\right)$$$

Lean4

@[to_additive]
theorem prod_union [DecidableEq ι] (h : Disjoint s₁ s₂) : ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x := by
  rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]; exact (mul_one _).symm

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