enumOfCountable_surjective
plain-language theorem explainer
The result shows that the enumeration map built from any inhabited countable type α is surjective from ℕ onto α. Lean users formalizing countable structures inside Recognition Science shims cite it to guarantee that enumerations cover every element. The argument extracts an injection witness via classical choice from the Countable hypothesis and verifies surjectivity by exhibiting the preimage under that injection.
Claim. Let $α$ be an inhabited type that admits a countability witness $h$. The map $enumOfCountable(h) : ℕ → α$ is surjective.
background
The module supplies shims for countability and equivalence constructions convenient for Lean 4 developments. It provides enumOfCountable to obtain a surjection ℕ → α from Countable α together with Inhabited α. The Countable assumption is the existence of an injection into ℕ; the shim converts that Prop-level witness into a Type-level function via Nonempty coercion and Classical.choice.
proof idea
The proof is a tactic script. It introduces an arbitrary a : α, invokes classical to access choice, extracts the injection f from h.exists_injective_nat, selects f a as witness, simplifies the definition of enumOfCountable, rewrites the dif_pos branch, and applies injectivity of f to finish.
why it matters
The theorem pairs with the definition of enumOfCountable to make the shim complete: the constructed map is both total and onto. It supports formal work that needs countable types without direct dependence on mathlib Encodable. No link to core Recognition Science landmarks such as the forcing chain T0-T8 or the Recognition Composition Law appears in the supplied facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.