mathlib documentation

data.fintype.card_embedding

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 β] [decidable_eq α] [decidable_eq β] :
@[simp]
theorem fintype.card_embedding_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] :
@[simp]
theorem fintype.card_embedding_eq_of_infinite {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] :
fintype.card β) = 0