Commit 2023-12-19 17:29 e851153f
View on Github →feat(Data/Finset/Card): the number of element satisfying P is no greater than n iff every subset with more than n elements contains an element not satisfying P (#9048)
feat(Data/Finset/Card): the number of element satisfying P is no greater than n iff every subset with more than n elements contains an element not satisfying P (#9048)