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.
α is infinite,
nat.card α = 0.
If the cardinality is positive, that means it is a finite type, so there is
an equivalence between
fin (nat.card α). See also