basic): A finset has card two iff it's `{x, y}` for some `x ≠ y` (#10252)

Commit

4 years ago

feat(data/finset/basic): A finset has card two iff it's `{x, y}` for some `x ≠ y` (#10252) and the similar result for card three. Dumb but surprisingly annoying!

Author

YaelDillies

Parents

9fe0cbc8

mathlib3 1a47cfc7 - feat(data/finset/basic): A finset has card two iff it's `{x, y}` for some `x ≠ y` (#10252)

mathlib3
1a47cfc7 - feat(data/finset/basic): A finset has card two iff it's `{x, y}` for some `x ≠ y` (#10252)