Theorem Finset.card_le_card_of_inj_on

Modification history

2024-06-12 09:13

Mathlib/Data/Finset/Card.lean

feat: Cardinality of a finset under a surjective map (#13435) …

Deleted Finset.card_le_card_of_inj_on View on Github →

2023-01-16 16:20

Mathlib/Data/Finset/Card.lean

feat: port Data.Finset.Card (#1589)

Added Finset.card_le_card_of_inj_on View on Github →