pred_eq_pred_iff_of_not_isMin

Mathlib.Order.SuccPred.Basic

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

← MathLib Explorer

English

If a and b are not minimal, then pred a = pred b iff a = b.

Русский

Если a и b не минимальны, то pred(a) = pred(b) эквивалентно a = b.

LaTeX

$$$\operatorname{pred} a = \operatorname{pred} b \iff a = b$$$

Lean4

theorem pred_eq_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) : pred a = pred b ↔ a = b := by
  rw [eq_iff_le_not_lt, eq_iff_le_not_lt, pred_le_pred_iff_of_not_isMin ha hb, pred_lt_pred_iff_of_not_isMin ha hb]

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

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

Разделы

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

Аффилиация

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