prod_filter_not_mul_prod_filter — Mathlib

English

The product over the not-p part times the product over the p part equals the full product, i.e., an alternative ordering of the split products.

Русский

Произведение по не-p и по p части равно полному произведению.

LaTeX

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

Lean4

@[to_additive]
theorem prod_filter_not_mul_prod_filter (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
  rw [mul_comm, prod_filter_mul_prod_filter_not]

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