mathlib3 documentation

data.fintype.card_embedding

Number of embeddings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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