Countable types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define a typeclass saying that a given
Sort* is countable. See also
for a version that singles out a specific encoding of elements of
α by natural numbers.
This file also provides a few instances of this typeclass. More instances can be found in other
Definition and basic properties #
α is countable if there exists an injective map
α → ℕ.
Instances of this typeclass
@[protected, nolint, instance]