refactor(data/finset): correct name sdiff_disjoint -> disjoint_sdiff;…

… add sdiff_disjoint
leanprover-community · Mar 5, 2019 · c0b1eb1 · c0b1eb1
1 parent b3c749b
commit c0b1eb1
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/src/data/finset.lean b/src/data/finset.lean
@@ -1588,9 +1588,12 @@ by simp only [disjoint_left, mem_union, or_imp_distrib, forall_and_distrib]
   disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u :=
 by simp only [disjoint_right, mem_union, or_imp_distrib, forall_and_distrib]
 
-lemma disjoint_sdiff {s t : finset α} : disjoint (t \ s) s :=
+lemma sdiff_disjoint {s t : finset α} : disjoint (t \ s) s :=
 disjoint_left.2 $ assume a ha, (mem_sdiff.1 ha).2
 
+lemma disjoint_sdiff {s t : finset α} : disjoint s (t \ s) :=
+sdiff_disjoint.symm
+
 lemma disjoint_bind_left {ι : Type*} [decidable_eq ι]
   (s : finset ι) (f : ι → finset α) (t : finset α) :
   disjoint (s.bind f) t ↔ (∀i∈s, disjoint (f i) t) :=

diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean
@@ -473,7 +473,7 @@ begin
     { simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm,
         add_sub_add_right_eq_sub] },
     simp only [this],
-    exact hde _ _ (h _ finset.disjoint_sdiff) (h _ finset.disjoint_sdiff) }
+    exact hde _ _ (h _ finset.sdiff_disjoint) (h _ finset.sdiff_disjoint) }
 end
 
 /- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a` -/