English
If p and q are predicates on s, then the product over elements with Xor' (p x) (q x) equals the product of the two partial products: ones with p and not q, and ones with q and not p.
Русский
Если p и q — предикаты на s, то произведение по элементам с Xor'(p x, q x) равно произведению по элементам с (p x ∧ ¬ q x) и (q x ∧ ¬ p x).
LaTeX
$$$\\prod_{x \\in s} f(x) \\text{ over } {\\rm Xor}'(p(x),q(x)) = \\left( \\prod_{x \\in s, p(x) \\land \\lnot q(x)} f(x) \\right) \\left( \\prod_{x \\in s, q(x) \\land \\lnot p(x)} f(x) \\right)$$$
Lean4
@[to_additive]
theorem prod_filter_xor (p q : ι → Prop) [DecidablePred p] [DecidablePred q] :
(∏ x ∈ s with (Xor' (p x) (q x)), f x) = (∏ x ∈ s with (p x ∧ ¬q x), f x) * (∏ x ∈ s with (q x ∧ ¬p x), f x) :=
by
classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
simp only [Xor']
