Number of embeddings

This file establishes the cardinality of α ↪ β in full generality.

theorem Fintype.card_embedding_eq_of_unique {α : Type u_1} {β : Type u_2} [Unique α] [Fintype β] [Fintype (α ↪ β)] : Fintype.card (α ↪ β) = Fintype.card β

@[simp]

theorem Fintype.card_embedding_eq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [emb : Fintype (α ↪ β)] : Fintype.card (α ↪ β) = Nat.descFactorial (Fintype.card β) (Fintype.card α)

theorem Fintype.card_embedding_eq_of_infinite {α : Type u_1} {β : Type u_2} [Infinite α] [Fintype β] [Fintype (α ↪ β)] : Fintype.card (α ↪ β) = 0

The cardinality of embeddings from an infinite type to a finite type is zero. This is a re-statement of the pigeonhole principle.