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 (α β)] :
theorem Fintype.card_embedding_eq_of_infinite {α : Type u_1} {β : Type u_2} [Infinite α] [Fintype β] [Fintype (α β)] :
Fintype.card (α β) = 0