add_natCast_lt

Mathlib.Algebra.Order.SuccPred

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

← MathLib Explorer

English

If x is succ-limit and y < x, then for every n ∈ N, y + n < x.

Русский

Если x — succ-limit и y < x, то для любого n ∈ N выполняется y + n < x.

LaTeX

$$$\\\\IsSuccLimit x \\\\land y < x \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, y + n < x.$$$

Lean4

theorem add_natCast_lt [AddMonoidWithOne α] [SuccAddOrder α] (hx : IsSuccLimit x) (hy : y < x) : ∀ n : ℕ, y + n < x :=
  hx.isSuccPrelimit.add_natCast_lt hy

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

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

Разделы

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

Аффилиация

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