succ_le_iff_eq_top

Mathlib.Order.SuccPred.Basic

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

English

succ a ≤ a if and only if a is the top element.

Русский

succ a ≤ a эквивалентно тому, что a является верхним элементом.

LaTeX

$$succ a \le a \iff a = \top$$

Lean4

theorem succ_le_iff_eq_top : succ a ≤ a ↔ a = ⊤ :=
  succ_le_iff_isMax.trans isMax_iff_eq_top

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

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

Разделы

Аффилиация

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