succ_pred

Mathlib.Order.SuccPred.Basic

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

English

There is at most one PredOrder structure on a given PartialOrder.

Русский

Существует не более одной структуры PredOrder на данном PartialOrder.

LaTeX

$$$ \\text{Subsingleton} (\\mathrm{PredOrder}\\ \\alpha)$$$

Lean4

theorem succ_pred [NoMinOrder α] (a : α) : succ (pred a) = a :=
  CovBy.succ_eq (pred_covBy _)

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

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

Разделы

Аффилиация

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