Commit 2024-07-16 16:36 81e59487

feat: add lemma not_mem_singleton_iff (#14443) The contrapositive (?) of the lemma

theorem mem_singleton_iff {a b : α} : a ∈ ({b} : Set α) ↔ a = b :=
  Iff.rfl

was missing. This PR adds

@[simp]
theorem not_mem_singleton_iff {a b : α} : a ∉ ({b} : Set α) ↔ a ≠ b :=
  Iff.rfl

which can be useful in avoiding extra have statements in other proofs.