Pigeonhole_Principle
Provedcombinatoricspigeonhole-principleproofwiki
If n items are placed into k containers where n > k, then at least one container has more than one item.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Pigeonhole_Principle {α β : Type _} [Fintype α] [Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ¬Function.Injective f := by sorrySource