Cardinalities of finite types

This file defines the cardinality Fintype.card α as the number of elements in (univ : Finset α). We also include some elementary results on the values of Fintype.card on specific types.

Main declarations

• Fintype.card α: Cardinality of a fintype. Equal to Finset.univ.card.
• Finite.surjective_of_injective: an injective function from a finite type to itself is also surjective.

def Fintype.card (α : Type u_4) [Fintype α] : ℕ

card α is the number of elements in α, defined when α is a fintype.

theorem Fintype.subtype_card {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) : card { x : α // p x } = s.card

theorem Fintype.card_of_subtype {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) [Fintype { x : α // p x }] : card { x : α // p x } = s.card

@[simp]

theorem Fintype.card_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : card ↑p = s.card

theorem Fintype.card_of_finset' {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) [Fintype ↑p] : card ↑p = s.card

theorem Fintype.ofEquiv_card {α : Type u_1} {β : Type u_2} [Fintype α] (f : α ≃ β) : card β = card α

theorem Fintype.card_congr {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (f : α ≃ β) : card α = card β

theorem Fintype.card_congr' {α β : Type u_4} [Fintype α] [Fintype β] (h : α = β) : card α = card β

theorem Fintype.card_ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] : card α = 1

Note: this lemma is specifically about Fintype.ofSubsingleton. For a statement about arbitrary Fintype instances, use either Fintype.card_le_one_iff_subsingleton or Fintype.card_unique.

@[simp]

theorem Fintype.card_unique {α : Type u_1} [Unique α] [h : Fintype α] : card α = 1

theorem Fintype.card_ofIsEmpty {α : Type u_1} [IsEmpty α] : card α = 0

Note: this lemma is specifically about Fintype.ofIsEmpty. For a statement about arbitrary Fintype instances, use Fintype.card_eq_zero.

@[simp]

theorem Set.toFinset_card {α : Type u_4} (s : Set α) [Fintype ↑s] : s.toFinset.card = Fintype.card ↑s

@[simp]

theorem Finset.card_univ {α : Type u_1} [Fintype α] : univ.card = Fintype.card α

theorem Finset.eq_univ_of_card {α : Type u_1} [Fintype α] (s : Finset α) (hs : s.card = Fintype.card α) : s = univ

theorem Finset.card_eq_iff_eq_univ {α : Type u_1} [Fintype α] (s : Finset α) : s.card = Fintype.card α ↔ s = univ

theorem Finset.card_le_univ {α : Type u_1} [Fintype α] (s : Finset α) : s.card ≤ Fintype.card α

theorem Finset.card_lt_univ_of_notMem {α : Type u_1} [Fintype α] {s : Finset α} {x : α} (hx : x ∉ s) : s.card < Fintype.card α

theorem Finset.card_lt_iff_ne_univ {α : Type u_1} [Fintype α] (s : Finset α) : s.card < Fintype.card α ↔ s ≠ univ

theorem Finset.card_compl_lt_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ.card < Fintype.card α ↔ s.Nonempty

theorem Finset.card_univ_diff {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) : (univ \ s).card = Fintype.card α - s.card

theorem Finset.card_compl {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) : sᶜ.card = Fintype.card α - s.card

@[simp]

theorem Finset.card_add_card_compl {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) : s.card + sᶜ.card = Fintype.card α

@[simp]

theorem Finset.card_compl_add_card {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) : sᶜ.card + s.card = Fintype.card α

theorem Finset.compl_eq_of_disjoint_of_card_add_eq {ι : Type u_4} [DecidableEq ι] [Fintype ι] {S₁ S₂ : Finset ι} (h : Disjoint S₁ S₂) (h' : S₁.card + S₂.card = univ.card) : S₁ᶜ = S₂

theorem Fintype.card_compl_set {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] [Fintype ↑sᶜ] : card ↑sᶜ = card α - card ↑s

theorem Fintype.card_subtype_eq {α : Type u_1} (y : α) [Fintype { x : α // x = y }] : card { x : α // x = y } = 1

theorem Fintype.card_subtype_eq' {α : Type u_1} (y : α) [Fintype { x : α // y = x }] : card { x : α // y = x } = 1

theorem Fintype.card_empty : card Empty = 0

theorem Fintype.card_pempty : card PEmpty.{u_4 + 1} = 0

theorem Fintype.card_unit : card Unit = 1

@[simp]

theorem Fintype.card_punit : card PUnit.{u_4 + 1} = 1

@[simp]

theorem Fintype.card_bool : card Bool = 2

@[simp]

theorem Fintype.card_ulift (α : Type u_4) [Fintype α] : card (ULift.{u_5, u_4} α) = card α

@[simp]

theorem Fintype.card_plift (α : Type u_4) [Fintype α] : card (PLift α) = card α

@[simp]

theorem Fintype.card_orderDual (α : Type u_4) [Fintype α] : card αᵒᵈ = card α

@[simp]

theorem Fintype.card_lex (α : Type u_4) [Fintype α] : card (Lex α) = card α

@[simp]

theorem Fintype.card_setUniv {α : Type u_1} [Fintype α] {h : Fintype ↑Set.univ} : card ↑Set.univ = card α

@[simp]

theorem Fintype.card_subtype_true {α : Type u_1} [Fintype α] {h : Fintype { _a : α // True }} : card { _a : α // True } = card α

@[implicit_reducible]

noncomputable def Fintype.sumLeft {α : Type u_4} {β : Type u_5} [Fintype (α ⊕ β)] : Fintype α

Given that α ⊕ β is a fintype, α is also a fintype. This is non-computable as it uses that Sum.inl is an injection, but there's no clear inverse if α is empty.

@[implicit_reducible]

noncomputable def Fintype.sumRight {α : Type u_4} {β : Type u_5} [Fintype (α ⊕ β)] : Fintype β

Given that α ⊕ β is a fintype, β is also a fintype. This is non-computable as it uses that Sum.inr is an injection, but there's no clear inverse if β is empty.

theorem Finite.exists_univ_list (α : Type u_4) [Finite α] : ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l

theorem List.Nodup.length_le_card {α : Type u_4} [Fintype α] {l : List α} (h : l.Nodup) : l.length ≤ Fintype.card α

theorem Fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (hf : Function.Injective f) : card α ≤ card β

theorem Fintype.not_injective_of_card_lt {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (h : card β < card α) : ¬Function.Injective f

theorem Fintype.card_le_of_embedding {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α ↪ β) : card α ≤ card β

theorem Fintype.card_lt_of_injective_of_notMem {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (h : Function.Injective f) {b : β} (w : b ∉ Set.range f) : card α < card β

theorem Fintype.card_lt_of_injective_not_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (h : Function.Injective f) (h' : ¬Function.Surjective f) : card α < card β

theorem Fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (h : Function.Surjective f) : card β ≤ card α

theorem Fintype.card_range_le {α : Type u_4} {β : Type u_5} (f : α → β) [Fintype α] [Fintype ↑(Set.range f)] : card ↑(Set.range f) ≤ card α

theorem Fintype.card_range {α : Type u_4} {β : Type u_5} {F : Type u_6} [FunLike F α β] [EmbeddingLike F α β] (f : F) [Fintype α] [Fintype ↑(Set.range ⇑f)] : card ↑(Set.range ⇑f) = card α

theorem Fintype.card_eq_zero_iff {α : Type u_1} [Fintype α] : card α = 0 ↔ IsEmpty α

@[simp]

theorem Fintype.card_eq_zero {α : Type u_1} [Fintype α] [IsEmpty α] : card α = 0

theorem Fintype.card_of_isEmpty {α : Type u_1} [Fintype α] [IsEmpty α] : card α = 0

Alias of Fintype.card_eq_zero.

def Fintype.cardEqZeroEquivEquivEmpty {α : Type u_1} [Fintype α] : card α = 0 ≃ (α ≃ Empty)

A Fintype with cardinality zero is equivalent to Empty.

theorem Fintype.card_pos_iff {α : Type u_1} [Fintype α] : 0 < card α ↔ Nonempty α

theorem Fintype.card_pos {α : Type u_1} [Fintype α] [h : Nonempty α] : 0 < card α

@[simp]

theorem Fintype.card_ne_zero {α : Type u_1} [Fintype α] [Nonempty α] : card α ≠ 0

instance Fintype.instNeZeroNatCardOfNonempty {α : Type u_1} [Fintype α] [Nonempty α] : NeZero (card α)

theorem Fintype.existsUnique_iff_card_one {α : Type u_4} [Fintype α] (p : α → Prop) [DecidablePred p] : (∃! a : α, p a) ↔ {x : α | p x}.card = 1

theorem Fintype.two_lt_card_iff {α : Type u_1} [Fintype α] : 2 < card α ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem Fintype.card_of_bijective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : α → β} (hf : Function.Bijective f) : card α = card β

theorem Finite.surjective_of_injective {α : Type u_1} [Finite α] {f : α → α} (hinj : Function.Injective f) : Function.Surjective f

theorem Finite.injective_iff_surjective {α : Type u_1} [Finite α] {f : α → α} : Function.Injective f ↔ Function.Surjective f

theorem Finite.injective_iff_bijective {α : Type u_1} [Finite α] {f : α → α} : Function.Injective f ↔ Function.Bijective f

theorem Finite.surjective_iff_bijective {α : Type u_1} [Finite α] {f : α → α} : Function.Surjective f ↔ Function.Bijective f

theorem Finite.injective_iff_surjective_of_equiv {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β) : Function.Injective f ↔ Function.Surjective f

theorem Function.Injective.bijective_of_finite {α : Type u_1} [Finite α] {f : α → α} : Injective f → Bijective f

Alias of the forward direction of Finite.injective_iff_bijective.

theorem Function.Surjective.bijective_of_finite {α : Type u_1} [Finite α] {f : α → α} : Surjective f → Bijective f

Alias of the forward direction of Finite.surjective_iff_bijective.

theorem Function.Injective.surjective_of_finite {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β) : Injective f → Surjective f

Alias of the forward direction of Finite.injective_iff_surjective_of_equiv.

theorem Function.Surjective.injective_of_finite {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β) : Surjective f → Injective f

Alias of the reverse direction of Finite.injective_iff_surjective_of_equiv.

@[deprecated Function.Injective.surjective_of_finite (since := "2025-11-28")]

theorem Function.Injective.surjective_of_fintype {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β) : Injective f → Surjective f

Alias of the forward direction of Finite.injective_iff_surjective_of_equiv.

---

Alias of the forward direction of Finite.injective_iff_surjective_of_equiv.

@[deprecated Function.Surjective.injective_of_finite (since := "2025-11-28")]

theorem Function.Surjective.injective_of_fintype {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β) : Surjective f → Injective f

Alias of the reverse direction of Finite.injective_iff_surjective_of_equiv.

---

Alias of the reverse direction of Finite.injective_iff_surjective_of_equiv.

@[simp]

theorem Fintype.card_coe {α : Type u_1} (s : Finset α) [Fintype ↥s] : card ↥s = s.card

theorem Finset.exists_superset_card_eq {α : Type u_1} [Fintype α] {n : ℕ} {s : Finset α} (hsn : s.card ≤ n) (hnα : n ≤ Fintype.card α) : ∃ (t : Finset α), s ⊆ t ∧ t.card = n

We can inflate a set s to any bigger size.

@[simp]

theorem Fintype.card_prop : card Prop = 2

theorem set_fintype_card_le_univ {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] : Fintype.card ↑s ≤ Fintype.card α

theorem set_fintype_card_eq_univ_iff {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] : Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

theorem Fintype.card_subtype_le {α : Type u_1} [Fintype α] (p : α → Prop) [Fintype { a : α // p a }] : card { x : α // p x } ≤ card α

theorem Fintype.card_subtype_lt {α : Type u_1} [Fintype α] {p : α → Prop} [Fintype { a : α // p a }] {x : α} (hx : ¬p x) : card { x : α // p x } < card α

theorem Fintype.card_subtype {α : Type u_1} [Fintype α] (p : α → Prop) [Fintype { a : α // p a }] [DecidablePred p] : card { x : α // p x } = {x : α | p x}.card

@[simp]

theorem Fintype.card_subtype_compl {α : Type u_1} [Fintype α] (p : α → Prop) [Fintype { x : α // p x }] [Fintype { x : α // ¬p x }] : card { x : α // ¬p x } = card α - card { x : α // p x }

theorem Fintype.card_subtype_mono {α : Type u_1} (p q : α → Prop) (h : p ≤ q) [Fintype { x : α // p x }] [Fintype { x : α // q x }] : card { x : α // p x } ≤ card { x : α // q x }

theorem Fintype.card_compl_eq_card_compl {α : Type u_1} [Finite α] (p q : α → Prop) [Fintype { x : α // p x }] [Fintype { x : α // ¬p x }] [Fintype { x : α // q x }] [Fintype { x : α // ¬q x }] (h : card { x : α // p x } = card { x : α // q x }) : card { x : α // ¬p x } = card { x : α // ¬q x }

If two subtypes of a fintype have equal cardinality, so do their complements.

theorem Fintype.card_quotient_le {α : Type u_1} [Fintype α] (s : Setoid α) [DecidableRel fun (x1 x2 : α) => x1 ≈ x2] : card (Quotient s) ≤ card α

theorem univ_eq_singleton_of_card_one {α : Type u_4} [Fintype α] (x : α) (h : Fintype.card α = 1) : Finset.univ = {x}

theorem Finite.wellFounded_of_trans_of_irrefl {α : Type u_1} [Finite α] (r : α → α → Prop) [IsTrans α r] [Std.Irrefl r] : WellFounded r

@[instance 100]

instance Finite.to_wellFoundedLT {α : Type u_1} [Finite α] [Preorder α] : WellFoundedLT α

@[instance 100]

instance Finite.to_wellFoundedGT {α : Type u_1} [Finite α] [Preorder α] : WellFoundedGT α

instance Bool.instWellFoundedLT : WellFoundedLT Bool

instance Bool.instWellFoundedGT : WellFoundedGT Bool

instance Prop.instWellFoundedLT : WellFoundedLT Prop

instance Prop.instWellFoundedGT : WellFoundedGT Prop

def truncOfCardPos {α : Type u_4} [Fintype α] (h : 0 < Fintype.card α) : Trunc α

A Fintype with positive cardinality constructively contains an element.

theorem Fintype.induction_subsingleton_or_nontrivial {P : (α : Type u_4) → [Fintype α] → Prop} (α : Type u_4) [Fintype α] (hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α) (hstep : ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α) : P α

A custom induction principle for fintypes. The base case is a subsingleton type, and the induction step is for non-trivial types, and one can assume the hypothesis for smaller types (via Fintype.card).

The major premise is Fintype α, so to use this with the induction tactic you have to give a name to that instance and use that name.

@[simp]

theorem Fintype.card_fin (n : ℕ) : card (Fin n) = n

theorem Fintype.card_fin_lt_of_le {m n : ℕ} (h : m ≤ n) : card { i : Fin n // ↑i < m } = m

theorem Finset.card_fin (n : ℕ) : univ.card = n

theorem fin_injective : Function.Injective Fin

Fin as a map from ℕ to Type is injective. Note that since this is a statement about equality of types, using it should be avoided if possible.

theorem Fin.val_eq_val_of_heq {k l : ℕ} {i : Fin k} {j : Fin l} (h : i ≍ j) : ↑i = ↑j

theorem Fin.cast_eq_cast' {n m : ℕ} (h : Fin n = Fin m) : cast h = Fin.cast ⋯

A reversed version of Fin.cast_eq_cast that is easier to rewrite with.

theorem card_finset_fin_le {n : ℕ} (s : Finset (Fin n)) : s.card ≤ n