Commit 2024-06-12 09:13 4ab4901e

feat: Cardinality of a finset under a surjective map (#13435) Prove a few easy (but annoying to prove on the fly) results about cardinality of finsets:

• If f is surjective from s to t, then t.card ≤ s.card.
• If two finsets t, u are subsets of s and s.card < t.card + u.card, then t and u are not disjoint. Rename Finset.card_le_card_of_inj_on to Finset.card_le_card_of_injOn and state it using Set.InjOn. Golf Finset.surj_on_of_inj_on_of_card_le. From LeanAPAP