one_lt_last

Mathlib.Data.Fin.Basic

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

← MathLib Explorer

English

For NeZero n, 1 < last(n+1).

Русский

Для НеНуля n, 1 < last(n+1).

LaTeX

$$$$1 < \mathrm{last}(n+1).$$$$

Lean4

theorem one_lt_last [NeZero n] : 1 < last (n + 1) :=
  by
  rw [lt_iff_val_lt_val, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]
  exact NeZero.ne n

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

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

Разделы

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

Аффилиация

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