Commit 2023-11-17 11:02 414c0c82

View on Github →

feat: Add Set.Nonempty.eq_zero and variations (#8423) See the Zulip thread

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.Nonempty.eq_one

added theorem Set.Nonempty.eq_zero

added theorem Set.eq_of_nonempty_of_subsingleton'

added theorem Set.eq_of_nonempty_of_subsingleton