succAbove_cases_eq_insertNth

Mathlib.Data.Fin.Tuple.Basic

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

English

The eliminator succAboveCases is equal to the insertion operator insertNth.

Русский

Элиминационная конструктор succAboveCases равен оператору вставки insertNth.

LaTeX

$$$\operatorname{succAboveCases} = \operatorname{insertNth}.$$$

Lean4

@[simp]
theorem succAbove_cases_eq_insertNth : @succAboveCases = @insertNth :=
  rfl

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

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

Разделы

Аффилиация

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