pred_succ_of_not_isMax

Mathlib.Order.SuccPred.Basic

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

English

pred ⊤ ≤ a iff a = ⊤ or a = pred ⊤.

Русский

pred ⊤ ≤ a эквивалентно a = ⊤ или a = pred ⊤.

LaTeX

$$$ pred\\top \\le a \\iff a = \\top \\lor a = pred\\top $$$

Lean4

@[simp]
theorem pred_succ_of_not_isMax (h : ¬IsMax a) : pred (succ a) = a :=
  CovBy.pred_eq (covBy_succ_of_not_isMax h)

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

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

Разделы

Аффилиация

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