enumOfCountable_surjective
The surjectivity of the enumeration map from naturals to an inhabited countable type is established by inverting the injection witness. Researchers formalizing countable structures in Recognition Science shims would cite this to guarantee onto mappings in equivalence constructions. The argument extracts the injection via Nonempty coercion and classical choice, then directly verifies the preimage for any target element using the injection property.
claimLet $α$ be an inhabited type with countability witness $h$. Then the map $enumOfCountable(h) : ℕ → α$ is surjective.
background
Shims.CountableEquiv supplies auxiliary constructions for countability in Lean developments. The definition enumOfCountable takes a countability proof $h$ for an inhabited type $α$ and produces a function from naturals to $α$ by extracting an injection into $ℕ$ via Nonempty and Classical.choice, then inverting it classically to define the surjection. This module avoids direct dependence on mathlib's Encodable by providing explicit constructive proofs. The upstream definition enumOfCountable handles the extraction of the injection witness from the Countable hypothesis, which is a Prop, by coercing to Nonempty.
proof idea
The proof fixes an arbitrary element $a$ in $α$. It extracts the injection $f : α → ℕ$ via classical choice from the countability witness. It then selects $f a$ as the preimage witness and applies the enumOfCountable construction, using the injection property to confirm that the chosen preimage recovers $a$.
why it matters in Recognition Science
This result completes the shim for obtaining surjections from countable types, supporting equivalence constructions in the broader Recognition Science formalization. It ensures the enumeration map is total and onto, which is prerequisite for downstream uses in mechanism design and simplicial ledgers. It aligns with the framework's need for clean countability handling without version-specific mathlib coupling.
scope and limits
- Does not provide a computable enumeration without classical axioms.
- Does not extend to uncountable types.
- Does not address decidability of membership in the image.
formal statement (Lean)
57theorem enumOfCountable_surjective {α : Type u} [Inhabited α] (h : Countable α) :
58 Function.Surjective (enumOfCountable h) := by
proof body
Term-mode proof.
59 intro a
60 classical
61 -- Extract the injection
62 let f_witness : Nonempty (∃ f : α → ℕ, Injective f) := ⟨h.exists_injective_nat⟩
63 let f_data := Classical.choice f_witness
64 let f := f_data.choose
65 let hinj := f_data.choose_spec
66 -- f a is in the range, so enumOfCountable (f a) = a
67 use f a
68 simp [enumOfCountable]
69 have hex : ∃ a', f a' = f a := ⟨a, rfl⟩
70 rw [dif_pos hex]
71 have hchoose := Classical.choose_spec hex
72 exact hinj hchoose
73
74end Shims