Theorems · Inductive type · logic and foundations

Encodable

Type u_1 → Type u_1

Constructively countable type. Made from an explicit injection encode : α → ℕ and a partial inverse decode : ℕ → Option α. Note that finite types are countable. See Denumerable if you wish to enforce infiniteness.

Defined in

Mathlib.Logic.Encodable.Basic

Cited by

140 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms