basic): a finset has card at most one iff it is contained in a singleton (#7404)

Commit

4 years ago

feat(data/finset/basic): a finset has card at most one iff it is contained in a singleton (#7404)

Author

sgouezel

Parents