fintypeArrowOfEncodable — Mathlib

English

If α is countable and finite and β is encodable, then α → β is encodable (explicit construction).

Русский

Если α счётен и конечен, а β кодируем, то α → β кодируемо (построение).

LaTeX

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

Lean4

/-- If `α` and `β` are encodable and `α` is a fintype, then `α → β` is encodable as well. -/
instance fintypeArrowOfEncodable {α β : Type*} [Encodable α] [Fintype α] [Encodable β] : Encodable (α → β) :=
  ofEquiv (Fin (Fintype.card α) → β) <| Equiv.arrowCongr fintypeEquivFin (Equiv.refl _)

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