feat(data/finset): erase is empty iff (#11838)

leanprover-community · Feb 5, 2022 · 612ca40 · 612ca40
1 parent 31f5688
commit 612ca40
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
@@ -1272,6 +1272,9 @@ lemma union_eq_sdiff_union_sdiff_union_inter (s t : finset α) :
   s ∪ t = (s \ t) ∪ (t \ s) ∪ (s ∩ t) :=
 sup_eq_sdiff_sup_sdiff_sup_inf
 
+lemma erase_eq_empty_iff (s : finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a} :=
+by rw [←sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
+
 end decidable_eq
 
 /-! ### attach -/