basic): A nonempty set of a subsingleton is `univ` (#16965)

Commit

3 years ago

feat(data/{finset,set}/basic): A nonempty set of a subsingleton is `univ` (#16965) Also provide `nonempty.coe_sort` and `nontrivial.coe_sort` aliases for dot notation.

Author

YaelDillies

Parents

43514e1e

mathlib3 5b294cfe - feat(data/{finset,set}/basic): A nonempty set of a subsingleton is `univ` (#16965)

mathlib3
5b294cfe - feat(data/{finset,set}/basic): A nonempty set of a subsingleton is `univ` (#16965)