countable_of_surjective
plain-language theorem explainer
A surjection from the naturals onto a type yields countability of that type. Lean formalizers building enumerations or handling infinite discrete structures cite this shim to obtain the Countable instance directly. The tactic proof invokes classical choice, defines the left inverse via Nat.find on the surjectivity witness, verifies the inverse property, proves injectivity by a three-step equality chain, and applies the Countable constructor.
Claim. Let $f : {N} → α$ be surjective. Then α is countable, meaning there exists an injection $g : α → {N}$.
background
The module supplies shims for countability and equivalence constructions convenient in Lean 4. Countable α is defined as the existence of an injection from α into the naturals. Surjective f means that for every element a in α there is some natural n with f n = a. The module notes that mathlib's Countable API works via Encodable or injections and provides these clean constructive proofs to reduce version coupling.
proof idea
The tactic proof begins with classical to permit choice. It defines g(a) as Nat.find (hf a), the least n such that f n = a. It records the left-inverse property f (g a) = a via Nat.find_spec. Injectivity of g is shown by a calc block: a1 equals f(g a1) which equals f(g a2) which equals a2 when g a1 = g a2. The proof concludes by applying the Countable constructor to the pair (g, hinj).
why it matters
This declaration supplies a direct, self-contained route from surjectivity to countability, supporting the module's aim of clear constructions. It pairs with the sibling enumOfCountable to establish the practical equivalence between countability and the existence of a surjection from the naturals. The result appears in formalizations that require explicit handling of countable sets arising in number-theoretic or combinatorial arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.