data.fincard
source
nat.card α
α
nat.card α = 0
enat.card α
enat.card α = ⊤
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 α = ⊤.