encodable

Mathlib.Logic.Encodable.Basic

URI: https://scilib.ai/kg/mathlib#Fin.encodable

English

The finite type Fin n is encodable; in fact Fin n is in bijection with the subtype {m ∈ ℕ | m < n} via Fin.equivSubtype.

Русский

Конечный тип Fin(n) кодируем: существует биекция Fin(n) ≃ {m ∈ ℕ | m < n} через Fin.equivSubtype.

LaTeX

$$$ \mathrm{Fin}(n) \cong \{ m \in \mathbb{N} \mid m < n \} $$$

Lean4

instance _root_.Fin.encodable (n) : Encodable (Fin n) :=
  ofEquiv _ Fin.equivSubtype

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

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

Разделы

Аффилиация

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