Documentation

Mathlib.Data.Fintype.CardEmbedding

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 (α β)] :
@[simp]
theorem Fintype.card_embedding_eq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [emb : Fintype (α β)] :
Fintype.card (α β) = (Fintype.card β).descFactorial (Fintype.card α)
theorem Fintype.card_embedding_eq_of_infinite {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β] [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.