feat(data/finset): to_finset_eq_empty

leanprover-community · Mar 31, 2019 · 514de77 · 514de77
1 parent 72634d2
commit 514de77
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/data/finset.lean b/src/data/finset.lean
@@ -717,6 +717,9 @@ finset.ext' $ by simp
   to_finset (s ∩ t) = to_finset s ∩ to_finset t :=
 finset.ext' $ by simp
 
+theorem to_finset_eq_empty {m : multiset α} : m.to_finset = ∅ ↔ m = 0 :=
+finset.val_inj.symm.trans multiset.erase_dup_eq_zero
+
 end multiset
 
 namespace list

diff --git a/src/data/multiset.lean b/src/data/multiset.lean
@@ -2321,6 +2321,10 @@ theorem erase_dup_eq_self {s : multiset α} : erase_dup s = s ↔ nodup s :=
 ⟨λ e, e ▸ nodup_erase_dup s,
  quot.induction_on s $ λ l h, congr_arg coe $ erase_dup_eq_self.2 h⟩
 
+theorem erase_dup_eq_zero {s : multiset α} : erase_dup s = 0 ↔ s = 0 :=
+⟨λ h, eq_zero_of_subset_zero $ h ▸ subset_erase_dup _,
+ λ h, h.symm ▸ erase_dup_zero⟩
+
 @[simp] theorem erase_dup_singleton {a : α} : erase_dup (a :: 0) = a :: 0 :=
 erase_dup_eq_self.2 $ nodup_singleton _