sub_one_lt_iff

Mathlib.Algebra.Group.Fin.Basic

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

← MathLib Explorer

English

For Fin(n+1), k - 1 < k iff 0 < k.

Русский

Для Fin(n+1) верно, что k−1 < k эквивалентно 0 < k.

LaTeX

$$$\\forall {n}, {k:\\mathrm{Fin}(n+1)},\\ k-1

Lean4

theorem sub_one_lt_iff {k : Fin (n + 1)} : k - 1 < k ↔ 0 < k :=
  not_iff_not.1 <| by simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

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

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

Разделы

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

Аффилиация

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