Commit 2025-10-23 00:03 87ab66e1

View on Github →

refactor: generalise Set.eq_empty_of_isEmpty (#30722) We don't need to know that the full type is empty, but merely the set itself.

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

modified theorem Set.eq_empty_of_isEmpty

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean