mathlib
78bc3724 - feat(data/{finset, set}/basic): tweak `nonempty_coe_sort` and `is_empty_coe_sort` (#14937)

Commit
3 years ago
feat(data/{finset, set}/basic): tweak `nonempty_coe_sort` and `is_empty_coe_sort` (#14937) This PR does the following: - add lemmas `set.is_empty_coe_sort` and `finset.is_empty_coe_sort` - made argument of both `nonempty_coe_sort` lemmas inferred - fix some spacing
Author
Parents
Loading