Theorem Set.eq_of_nonempty_of_subsingleton

Modification history

2023-11-17 11:02
Mathlib/Data/Set/Basic.lean
feat: Add Set.Nonempty.eq_zero and variations (#8423) …
Added Set.eq_of_nonempty_of_subsingletonView on Github →