From b56f7a06d59edc9f3cd2cf3eee3390b1585adbad Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 8 May 2015 20:06:21 +1000 Subject: [PATCH] refactor(library/data/finset/bigop.lean): use inter eq empty rather than disjoint --- library/data/finset/bigop.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/library/data/finset/bigop.lean b/library/data/finset/bigop.lean index c03814e172..fa728a1742 100644 --- a/library/data/finset/bigop.lean +++ b/library/data/finset/bigop.lean @@ -32,7 +32,10 @@ theorem bigop_insert_of_not_mem (f : A → B) {a : A} {s : finset A} : a ∉ s quot.induction_on s (λ l nainl, list.bigop_insert_of_not_mem f nainl) -theorem bigop_union (f : A → B) {s₁ s₂ : finset A} : disjoint s₁ s₂ → bigop (s₁ ∪ s₂) f = bigop s₁ f * bigop s₂ f := -quot.induction_on₂ s₁ s₂ - (λ l₁ l₂ d, list.bigop_union f d) +theorem bigop_union (f : A → B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : +bigop (s₁ ∪ s₂) f = bigop s₁ f * bigop s₂ f := +have H1 : disjoint s₁ s₂ → bigop (s₁ ∪ s₂) f = bigop s₁ f * bigop s₂ f, from + quot.induction_on₂ s₁ s₂ + (λ l₁ l₂ d, list.bigop_union f d), +H1 (disjoint_of_inter_empty disj) end finset