Pigeonhole

Statistics

Metric	Count
Definitions	0
Theorems `card_range_le`, `le_of_embedding`, `le_of_injective`, `le_of_surjective`, `lt_of_injective_of_notMem`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`card_range_le` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Set.range` `Subtype.fintype` `Set` `Set.instMembership` `Fintype.decidableMemRangeFintype` `fintype`	—	`Fintype.card_ofFinset` `Fintype.card_fin` `Fintype.card_range_le`
`le_of_embedding` 📖	—	—	—	—	`Fintype.card_fin` `Fintype.card_le_of_embedding`
`le_of_injective` 📖	—	—	—	—	`Fintype.card_fin` `Fintype.card_le_of_injective`
`le_of_surjective` 📖	—	—	—	—	`Fintype.card_fin` `Fintype.card_le_of_surjective`
`lt_of_injective_of_notMem` 📖	—	`Set` `Set.instMembership` `Set.range`	—	—	`Fintype.card_fin` `Fintype.card_lt_of_injective_of_notMem`

---