Theorem Set.exists_mem_singleton

Modification history

2026-08-16 17:38
Mathlib/Data/Set/Insert.lean
chore(Data/Set): add missing `Set.forall_mem_*` lemmas (#42549) …
Added Set.exists_mem_singletonView on Github →