136theorem finite_function_is_computable {α β : Type*} [Fintype α] [Fintype β] 137 [DecidableEq α] [DecidableEq β] 138 (f : α → β) : 139 ∃ (table : Finset (α × β)), 140 ∀ a : α, ∃ b : β, (a, b) ∈ table ∧ f a = b := by
proof body
Term-mode proof.
141 use Finset.image (fun a => (a, f a)) Finset.univ 142 intro a 143 exact ⟨f a, Finset.mem_image.mpr ⟨a, Finset.mem_univ a, rfl⟩, rfl⟩ 144 145/-- **THEOREM IC-003.11**: The 8-tick step function is computable (it's a function 146 on a finite phase space, hence encodable as a lookup table). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.