Commit 2022-10-25 00:26 5b294cfe
View on Github →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.
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.