basic): generalize some lemmas to `Sort*` (#17503)

Commit

3 years ago

chore(data/fintype/basic): generalize some lemmas to `Sort*` (#17503) Also add `function.embedding.nonempty_iff_card_le`.

Author

urkud

Parents