# mathlib3documentation

set_theory.cardinal.finite

# Finite Cardinality Functions #

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

## Main Definitions #

• nat.card α is the cardinality of α as a natural number. If α is infinite, nat.card α = 0.
• part_enat.card α is the cardinality of α as an extended natural number (part ℕ implementation). If α is infinite, part_enat.card α = ⊤.
@[protected]
noncomputable def nat.card (α : Type u_1) :

nat.card α is the cardinality of α as a natural number. If α is infinite, nat.card α = 0.

Equations
@[simp]
theorem nat.card_eq_fintype_card {α : Type u_1} [fintype α] :
@[simp]
theorem nat.card_eq_zero_of_infinite {α : Type u_1} [infinite α] :
= 0
theorem nat.finite_of_card_ne_zero {α : Type u_1} (h : 0) :
theorem nat.card_congr {α : Type u_1} {β : Type u_2} (f : α β) :
theorem nat.card_eq_of_bijective {α : Type u_1} {β : Type u_2} (f : α β) (hf : function.bijective f) :
theorem nat.card_eq_of_equiv_fin {α : Type u_1} {n : } (f : α fin n) :
= n
noncomputable def nat.equiv_fin_of_card_pos {α : Type u_1} (h : 0) :
α fin (nat.card α)

If the cardinality is positive, that means it is a finite type, so there is an equivalence between α and fin (nat.card α). See also finite.equiv_fin.

Equations
theorem nat.card_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :
= 1
@[simp]
theorem nat.card_unique {α : Type u_1} [unique α] :
= 1
theorem nat.card_eq_one_iff_unique {α : Type u_1} :
= 1
theorem nat.card_eq_two_iff {α : Type u_1} :
= 2 (x y : α), x y {x, y} = set.univ
theorem nat.card_eq_two_iff' {α : Type u_1} (x : α) :
= 2 ∃! (y : α), y x
theorem nat.card_of_is_empty {α : Type u_1} [is_empty α] :
= 0
@[simp]
theorem nat.card_prod (α : Type u_1) (β : Type u_2) :
nat.card × β) =
@[simp]
theorem nat.card_ulift (α : Type u_1) :
@[simp]
theorem nat.card_plift (α : Type u_1) :
theorem nat.card_pi {α : Type u_1} {β : α Type u_2} [fintype α] :
nat.card (Π (a : α), β a) = finset.univ.prod (λ (a : α), nat.card (β a))
theorem nat.card_fun {α : Type u_1} {β : Type u_2} [finite α] :
nat.card β) =
@[simp]
theorem nat.card_zmod (n : ) :
noncomputable def part_enat.card (α : Type u_1) :

part_enat.card α is the cardinality of α as an extended natural number. If α is infinite, part_enat.card α = ⊤.

Equations
@[simp]
theorem part_enat.card_eq_coe_fintype_card {α : Type u_1} [fintype α] :
@[simp]
theorem part_enat.card_eq_top_of_infinite {α : Type u_1} [infinite α] :
theorem part_enat.card_congr {α : Type u_1} {β : Type u_2} (f : α β) :
theorem part_enat.card_ulift (α : Type u_1) :
@[simp]
theorem part_enat.card_plift (α : Type u_1) :
theorem part_enat.card_image_of_inj_on {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} (h : s) :
theorem part_enat.card_image_of_injective {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) (h : function.injective f) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem cardinal.coe_nat_lt_coe_iff_lt {n : } {c : cardinal} :
n < c
@[simp]
theorem cardinal.lt_coe_nat_iff_lt {n : } {c : cardinal} :
c < n
theorem part_enat.is_finite_of_card {α : Type u_1} {n : } (hα : = n) :