Pigeonhole

📁 Source: Mathlib/Data/Fintype/Pigeonhole.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_infinite_fiber, exists_ne_map_eq_of_infinite, exists_ne_map_eq_of_card_lt, isEmpty_of_card_lt	4
Total	4

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_infinite_fiber 📖	mathematical	—	Infinite Set.Elem Set.preimage Set Set.instSingletonSet	—	nonempty_fintype Fintype.false
exists_ne_map_eq_of_infinite 📖	—	—	—	—	not_injective_infinite_finite

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_ne_map_eq_of_card_lt 📖	—	card	—	—	Finset.exists_ne_map_eq_of_card_lt_of_maps_to Finset.mem_univ

Function.Embedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmpty_of_card_lt 📖	mathematical	Fintype.card	IsEmpty Function.Embedding	—	Fintype.exists_ne_map_eq_of_card_lt injective

---

← Back to Index