ofFn_id

Mathlib.Data.List.FinRange

URI: https://scilib.ai/kg/mathlib#List.ofFn_id

English

For any n, the list built from the identity on Fin n equals the standard FinRange: ofFn id = finRange n.

Русский

Для любого n список, построенный по тождественному отображению на Fin n, равен стандартному FinRange: ofFn id = finRange n.

LaTeX

$$$$ \\operatorname{ofFn}(\\mathrm{id}) = \\mathrm{finRange}(n). $$$$

Lean4

theorem ofFn_id (n) : ofFn id = finRange n :=
  rfl

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

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

Разделы

Аффилиация

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