prod_sdiff — Mathlib

English

If s1 ⊆ s2, then the product over s2 \\ s1 times the product over s1 equals the product over s2.

Русский

Если s1 ⊆ s2, то произведение по s2 \ s1 на произведение по s1 равно произведению по s2.

LaTeX

$$$\\prod_{x \\in s_2 \\setminus s_1} f(x) \\;\\cdot\\; \\prod_{x \\in s_1} f(x) = \\prod_{x \\in s_2} f(x)$$$

Lean4

@[to_additive]
theorem prod_sdiff [DecidableEq ι] (h : s₁ ⊆ s₂) : (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x := by
  rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]

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