Theorem Set.eq_empty_of_isEmpty

Modification history

2025-10-23 00:03

Mathlib/Data/Set/Basic.lean

refactor: generalise `Set.eq_empty_of_isEmpty` (#30722) …

Modified Set.eq_empty_of_isEmpty View on Github →

2022-12-12 01:34

Mathlib/Data/Set/Basic.lean

feat: port Data.Set.Basic (#892) …

Added Set.eq_empty_of_isEmpty View on Github →