lt_succ_iff_not_isMax

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.lt_succ_iff_not_isMax

← MathLib Explorer

English

An element is strictly less than its successor exactly when it is not maximal.

Русский

Элемент меньше своего продвижения ровно тогда, когда он не максимален.

LaTeX

$$$a < \\operatorname{succ}(a) \\iff \\neg \\mathrm{IsMax}(a)$$$

Lean4

@[simp]
theorem lt_succ_iff_not_isMax : a < succ a ↔ ¬IsMax a :=
  ⟨not_isMax_of_lt, fun ha => (le_succ a).lt_of_not_ge fun h => ha <| max_of_succ_le h⟩

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

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

Разделы

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

Аффилиация

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