From c81be77b8d60118a7756479601d252991251f90b Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Sat, 16 May 2020 14:49:11 +0000 Subject: [PATCH] feat(data/finset) Another finset disjointness lemma (#2698) I couldn't find this anywhere, and I wanted it. Naming question: this is "obviously" called `disjoint_filter`, except there's already a lemma with that name. I know I've broken one of the rules of using `simp` here ("don't do it at the beginning"), but this proof is much longer than I'd have thought would be necessary so I'm rather expecting someone to hop in with a one-liner. --- src/data/finset.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/data/finset.lean b/src/data/finset.lean index 4bc87379e757d..f3eac9a819285 100644 --- a/src/data/finset.lean +++ b/src/data/finset.lean @@ -2562,6 +2562,10 @@ lemma disjoint_filter {s : finset α} {p q : α → Prop} [decidable_pred p] [de disjoint (s.filter p) (s.filter q) ↔ (∀ x ∈ s, p x → ¬ q x) := by split; simp [disjoint_left] {contextual := tt} +lemma disjoint_filter_filter {s t : finset α} {p q : α → Prop} [decidable_pred p] [decidable_pred q] : + (disjoint s t) → disjoint (s.filter p) (t.filter q) := +disjoint.mono (filter_subset _) (filter_subset _) + lemma pi_disjoint_of_disjoint {δ : α → Type*} [∀a, decidable_eq (δ a)] {s : finset α} [decidable_eq (Πa∈s, δ a)] (t₁ t₂ : Πa, finset (δ a)) {a : α} (ha : a ∈ s) (h : disjoint (t₁ a) (t₂ a)) :