succ_eq_iff_isMax

Mathlib.Order.SuccPred.Basic

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

English

succ a = a if and only if a is maximal.

Русский

succ a = a тогда и только тогда, когда a максимально.

LaTeX

$$succ a = a \iff IsMax a$$

Lean4

@[simp]
theorem succ_eq_iff_isMax : succ a = a ↔ IsMax a :=
  ⟨fun h => max_of_succ_le h.le, fun h => h.eq_of_ge <| le_succ _⟩

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

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

Разделы

Аффилиация

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