prod_disjUnion — Mathlib

English

For two finite sets s1 and s2 that are disjoint, the product over their disjoint union equals the product of the two separate products.

Русский

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

LaTeX

$$$\\text{Disjoint}(s_1,s_2) \\Rightarrow \\prod_{x\\in s_1 \\sqcup 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_disjUnion (h) : ∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x :=
  by
  refine Eq.trans ?_ (fold_disjUnion h)
  rw [one_mul]
  rfl

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