fintypeArrow — Mathlib

English

If α is finite and β is encodable, then α → β is encodable up to truncation.

Русский

Если α конечен и β кодируем, то α → β кодируем с учетом усечения.

LaTeX

$$$ \\text{Trunc}(\\text{Encodable}(\\alpha \\to \\beta)). $$$

Lean4

/-- When `α` is finite and `β` is encodable, `α → β` is encodable too. Because the encoding is not
unique, we wrap it in `Trunc` to preserve computability. -/
def fintypeArrow (α : Type*) (β : Type*) [DecidableEq α] [Fintype α] [Encodable β] : Trunc (Encodable (α → β)) :=
  (Fintype.truncEquivFin α).map fun f =>
    Encodable.ofEquiv (Fin (Fintype.card α) → β) <| Equiv.arrowCongr f (Equiv.refl _)

Похожие утверждения