mathlib documentation

set_theory.cardinal.finite

Finite Cardinality Functions #

Main Definitions #

@[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 α] :
nat.card α = 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) :
nat.card α = n
noncomputable def nat.equiv_fin_of_card_pos {α : Type u_1} (h : nat.card α 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 α] :
nat.card α = 1
@[simp]
theorem nat.card_unique {α : Type u_1} [unique α] :
nat.card α = 1
theorem nat.card_eq_one_iff_unique {α : Type u_1} :
theorem nat.card_of_is_empty {α : Type u_1} [is_empty α] :
nat.card α = 0
@[simp]
theorem nat.card_prod (α : Type u_1) (β : Type u_2) :
nat.card × β) = nat.card α * 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))
@[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]
@[simp]
theorem part_enat.card_eq_top_of_infinite {α : Type u_1} [infinite α] :