mathlib
bd59f822 - feat(data/set/basic): A set is either a subsingleton or nontrivial (#17901)

Commit
3 years ago
feat(data/set/basic): A set is either a subsingleton or nontrivial (#17901) Also make the argument to `set.finite_or_infinite` explicit.
Author
Parents
Loading