mathlib documentation

set_theory.fincard

Finite Cardinality Functions #

Main Definitions #

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
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 α] :