From 32d9c90a14734a2dfe178ca55d32b77d90d7c8cd Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Wed, 4 Dec 2024 06:45:09 +0000 Subject: [PATCH] prod_disjoint_filters_on_set --- Mathlib/Algebra/BigOperators/Group/Finset.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean index c235e6c2bd74a..4890049185511 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset.lean @@ -403,6 +403,17 @@ theorem prod_disjiUnion (s : Finset ι) (t : ι → Finset α) (h) : congr exact prod_const_one.symm +@[to_additive] +theorem prod_disjoint_filters_on_set (s : Finset α) (p q : α → Prop) [DecidablePred p] + [DecidablePred q] (h : ∀ x ∈ s.filter (fun x => p x ∨ q x), ¬ (p x ∧ q x)) (f : α → β) : + (∏ x ∈ s with (p x ∨ q x), f x) = (∏ x ∈ s with p x, f x) * (∏ x ∈ s with q x, f x) := by + rw [← prod_disjUnion (disjoint_of_not_and_on_set (fun x ↦ p x) (fun x ↦ q x) h)] + exact prod_congr (by + ext _ + simp only [mem_filter, mem_disjUnion] + exact and_or_left + ) (fun _ _ ↦ rfl) + @[to_additive] theorem prod_union_inter [DecidableEq α] : (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x :=