add_one_lt

Mathlib.Algebra.Order.SuccPred

URI: https://scilib.ai/kg/mathlib#Order.IsSuccLimit.add_one_lt

English

If x is a succ-limit and y < x, then y + 1 < x.

Русский

Если x — succ-limit и y < x, то y + 1 < x.

LaTeX

$$$\\\\IsSuccLimit x \\\\land y < x \\\\Rightarrow y + 1 < x.$$$

Lean4

theorem add_one_lt [Add α] [One α] [SuccAddOrder α] (hx : IsSuccLimit x) (hy : y < x) : y + 1 < x :=
  hx.isSuccPrelimit.add_one_lt hy

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

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

Разделы

Аффилиация

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