injection to show cardinality inquality

Stream: Is there code for X?

[George Shakan]

I would like a statement of the form: to show |X| <= |Y| it is enough to show there exists an injection from X to Y

[Jakub Kądziołka]

Is that for finite cardinalities?

[Jakub Kądziołka]

(otherwise it feels true by definition)

[Reid Barton]

docs#cardinal.mk_le_of_injective

[Bhavik Mehta]

docs#finset.card_le_card_of_inj_on