Finite Cardinality Functions #

Main Definitions #

nat.card α is the cardinality of α as a natural number. If α is infinite, nat.card α = 0.
enat.card α is the cardinality of α as an extended natural number. If α is infinite, 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 α] :

noncomputable def enat.card (α : Type u_1) :

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

Equations

@[simp]

theorem enat.card_eq_coe_fintype_card {α : Type u_1} [fintype α] :

@[simp]

theorem enat.card_eq_top_of_infinite {α : Type u_1} [infinite α] :