insertNthEquiv_zero

Mathlib.Data.Fin.Tuple.Basic

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

← MathLib Explorer

English

The 0-th position reduces to the standard cons-equivalence.

Русский

0-я позиция сводится к стандартной консолирующей эквивалентности.

LaTeX

$$$$ \mathrm{insertNthEquiv} \ α \, 0 = \mathrm{consEquiv} \ α $$$$

Lean4

@[simp]
theorem insertNthEquiv_zero (α : Fin (n + 1) → Type*) : insertNthEquiv α 0 = consEquiv α :=
  Equiv.symm_bijective.injective <| by ext <;> rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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