Commit 2025-10-28 10:18 e0f1e8d7

View on Github →

feat(Order/Cover): empty_covBy_singleton (#30915)

Estimated changes

Modified Mathlib/Data/Finset/Grade.lean

added theorem Finset.empty_covBy_singleton

Modified Mathlib/Order/Cover.lean

added theorem Set.empty_covBy_singleton