ofFin_toFin

Mathlib.Data.Fin.Fin2

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

English

Applying ofFin to a Fin2 element obtained from toFin yields the original Fin2 element.

Русский

Применение ofFin к Fin2-элементу, полученному из toFin, возвращает исходный Fin2-элемент.

LaTeX

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

Lean4

@[simp]
theorem ofFin_toFin {n : Nat} (i : Fin2 n) : ofFin (toFin i) = i := by
  induction i with
  | fz => rfl
  | fs _ ih => exact congrArg fs ih

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

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

Разделы

Аффилиация

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