mathlib
f66a5ddb - chore(data/set/basic): add a few lemmas and a `@[simp]` attribute (#12176)

Commit
3 years ago
chore(data/set/basic): add a few lemmas and a `@[simp]` attribute (#12176) * rename `set.exists_eq_singleton_iff_nonempty_unique_mem` to `set.exists_eq_singleton_iff_nonempty_subsingleton`, use `set.subsingleton` in the statement; * add `@[simp]` to `set.subset_compl_singleton_iff`; * add `set.diff_diff_right_self`.
Author
Parents
Loading