feat(data/set): sep true/false simp lemmas (#7215)

leanprover-community · Apr 16, 2021 · 49040e5 · 49040e5
1 parent 24013e2
commit 49040e5
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
@@ -754,6 +754,12 @@ theorem forall_not_of_sep_empty {s : set α} {p : α → Prop} (H : {x ∈ s | p
 @[simp] lemma subset_singleton_iff {α : Type*} {s : set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
 iff.rfl
 
+@[simp] lemma sep_true : {a ∈ s | true} = s :=
+by { ext, simp }
+
+@[simp] lemma sep_false : {a ∈ s | false} = ∅ :=
+by { ext, simp }
+
 /-! ### Lemmas about complement -/
 
 theorem mem_compl {s : set α} {x : α} (h : x ∉ s) : x ∈ sᶜ := h