last_sub

Mathlib.Data.Fin.Basic

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

← MathLib Explorer

English

For i ∈ Fin(n+1), last n − i equals rev i.

Русский

Для i ∈ Fin(n+1) последний элемент минус i равен обратному i.

LaTeX

$$$\\forall i : \\mathrm{Fin}(n+1), \\mathrm{last}\ n - i = \\mathrm{rev}\ i$$$

Lean4

theorem last_sub (i : Fin (n + 1)) : last n - i = Fin.rev i :=
  Fin.ext <| by rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]

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

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

Разделы

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

Аффилиация

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