Theorems · Definition · logic and foundations

Encodable.fintypeArrow

(α : Type u_2) → (β : Type u_3) → [DecidableEq α] → [Fintype α] → [Encodable β] → Trunc (Encodable (α → β))

When α is finite and β is encodable, α → β is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

Defined in

Mathlib.Logic.Encodable.Pi

Cited by

0 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeEncodable