enumOfCountable
plain-language theorem explainer
A definition that produces a surjection from the natural numbers onto any inhabited countable type. Researchers formalizing countable sets in Lean would cite it to obtain explicit enumerations. The construction extracts an injection witness via Nonempty coercion and Classical.choice, then inverts it by selecting preimages or falling back to the default inhabitant.
Claim. Given an inhabited type $α$ that is countable, the function $ℕ → α$ is constructed by classically inverting an injection from $α$ to $ℕ$ whose existence follows from countability, returning a chosen preimage when it exists and the default element of $α$ otherwise.
background
The Shims.CountableEquiv module provides auxiliary definitions for handling countability in Lean 4 developments. Countable $α$ denotes the existence of an injective map $α → ℕ$. An Inhabited instance on $α$ supplies the default value needed to complete the surjection. This approach decouples the construction from mathlib internals by using direct classical choice on the injection witness. The module documentation emphasizes clean constructive proofs to avoid version coupling.
proof idea
The body coerces the countability hypothesis to a Nonempty existential, selects a concrete injection with Classical.choice, and defines the map pointwise: if $n$ lies in the image of the injection then return a classical choice of preimage, otherwise return the default inhabitant.
why it matters
It supplies the concrete map whose surjectivity is established by the companion theorem proving surjectivity of the constructed enumeration. The shim supports equivalence constructions within the module by providing enumerations from countable types. It addresses the need for explicit surjections in formal proofs that treat countability as a Prop-level assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.