Structures · Logic and sets
Denumerable
A denumerable type is (constructively) bijective with ℕ. Typeclass equivalent of α ≃ ℕ.
- Defined in
- Mathlib.Logic.Denumerable
- Shape
- One type argument · adds decode_inv
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Denumerable is also a
Concrete types that are instances14
- Int
- Nat
- Rat
- PNat
- Nat.Partrec.Code
- Prod
- ULift
- Sum
- List
- Sigma
- Multiset
- Finset
- Option
- PLift
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- Denumerable.ofNat
- Denumerable.decode_eq_ofNat
- Denumerable.ofNat_encode
- Denumerable.sigma_ofNat_val
- Denumerable.ofEquiv_ofNat
- Primrec.ofNat
- Denumerable.eqv
- Cardinal.mk_denumerable
- Denumerable.ofNat_of_decode
- Computable.ofNat
- Primrec.ofNat_iff
- Primrec₂.ofNat_iff
- Denumerable.encode_ofNat
- Primrec.dom_denumerable
- Denumerable.decode_inv
- Computable.eqv
- Denumerable.decode_isSome
- Denumerable.prod_ofNat_val
- Denumerable.ofEquiv
- Denumerable.equiv₂
- Denumerable.ulift
- Denumerable.list_ofNat_succ
- Denumerable.finset
- Denumerable.toEncodable
- Denumerable.sigma
- Denumerable.denumerableList
- Denumerable.option
- Denumerable.prod
- Computable.equiv₂
- Denumerable.instInfinite
- Denumerable.multiset
- Denumerable.plift
- ProbabilityTheory.Kernel.isSFiniteKernel_sum_of_denumerable
- Primcodable.ofDenumerable
- Denumerable.list_ofNat_zero
- Denumerable.sum
- Denumerable.denumerable_list_aux
- Denumerable.pair