ofFin_succ

Mathlib.Data.Fin.Fin2

URI: https://scilib.ai/kg/mathlib#Fin2.ofFin_succ

English

The image of i.succ under Fin2.ofFin is the successor of the image of i.

Русский

Изображение i.succ через Fin2.ofFin равно successor от изображения i.

LaTeX

$$$\mathrm{Fin2\text{-}ofFin}(i\mathrm{.succ}) = \mathrm{fs}(\mathrm{Fin2\text{-}ofFin}(i)).$$$

Lean4

@[simp]
theorem ofFin_succ {n : Nat} (i : Fin n) : ofFin i.succ = fs (ofFin i) :=
  rfl

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

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

Разделы

Аффилиация

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