prod_filter_mul_prod_filter_not — Mathlib

English

If s is a finite set and p is a predicate, then the product over elements of s with p times the product over elements with not p equals the product over all of s.

Русский

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

LaTeX

$$$\\left( \\prod_{x \\in s \\text{ with } p(x)} f(x) \\right) \\cdot \\left( \\prod_{x \\in s \\text{ with } \\neg p(x)} f(x) \\right) = \\prod_{x \\in s} f(x)$$$

Lean4

@[to_additive]
theorem prod_filter_mul_prod_filter_not (s : Finset ι) (p : ι → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)]
    (f : ι → M) : (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x :=
  by
  have := Classical.decEq ι
  rw [← prod_union (disjoint_filter_filter_neg s s p), filter_union_filter_neg_eq]

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