finArrow

Mathlib.Logic.Encodable.Pi

URI: https://scilib.ai/kg/mathlib#Encodable.finArrow

← MathLib Explorer

English

If α is encodable, then Fin n → α is encodable for any n.

Русский

Если α кодируемо, то Fin n → α кодируемо для любого n.

LaTeX

$$$ [\\Encodable(\\,Fin\\ n\\to α\\,)] $$$

Lean4

/-- If `α` is encodable, then so is `Fin n → α`. -/
instance finArrow [Encodable α] {n} : Encodable (Fin n → α) :=
  ofEquiv _ (Equiv.vectorEquivFin _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru