finSumFinEquiv_symm_last

Mathlib.Logic.Equiv.Fin.Basic

URI: https://scilib.ai/kg/mathlib#finSumFinEquiv_symm_last

English

The inverse of the bijection sends Fin.last(n) to inr 0.

Русский

Обратное отображение биекции отправляет Fin.last(n) в inr 0.

LaTeX

$$$ finSumFinEquiv.symm (Fin.last n) = Sum.inr 0 $$$

Lean4

@[simp]
theorem finSumFinEquiv_symm_last : finSumFinEquiv.symm (Fin.last n) = Sum.inr 0 :=
  finSumFinEquiv_symm_apply_natAdd 0

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

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

Разделы

Аффилиация

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