michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/finset/bigop.lean): use inter eq empty rather than disjoint

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-08 20:06:21 +10:00
parent 9beb70b292
commit b56f7a06d5
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/data/finset/bigop.lean
View file

@ -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