encodable

Mathlib.Logic.Encodable.Pi

URI: https://scilib.ai/kg/mathlib#Encodable.List.Vector.encodable

English

If α is encodable, then List.Vector α n is encodable for any fixed n.

Русский

Если множество α кодируемо, то вектор List.Vector α n кодируем.

LaTeX

$$$ [\\Encodable(\\text{List.Vector } \\alpha n)]\\text{ holds when }[\\Encodable\\alpha]. $$$

Lean4

/-- If `α` is encodable, then so is `Vector α n`. -/
instance encodable [Encodable α] {n} : Encodable (List.Vector α n) :=
  Subtype.encodable

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

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

Разделы

Аффилиация

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