lt_add_one_of_succ_lt

Mathlib.Algebra.Group.Fin.Basic

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

← MathLib Explorer

English

If a+1 < n then a < a+1 in Fin n.

Русский

Если a+1 < n, то в Fin n выполняется a < a+1.

LaTeX

$$$\\forall n\\, [\\mathrm{NeZero}(n)]\\;\\{a:\\mathrm{Fin}(n)\\},\\; a+1< n\\Rightarrow a

Lean4

theorem lt_add_one_of_succ_lt {n : ℕ} [NeZero n] {a : Fin n} (ha : a + 1 < n) : a < a + 1 :=
  by
  rw [lt_def, val_add, coe_ofNat_eq_mod, Nat.add_mod_mod, Nat.mod_eq_of_lt ha]
  cutsat

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

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

Разделы

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

Аффилиация

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