pred_lt_iff_of_not_isMin

Mathlib.Order.SuccPred.Basic

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

English

If a is not minimal, then for all b, pred(a) < b iff a ≤ b.

Русский

Если a не минимален, то для любого b верно: pred(a) < b эквивалентно a ≤ b.

LaTeX

$$$\operatorname{pred} a < b \iff a \le b \quad (\text{when } \neg \operatorname{IsMin}(a))$$$

Lean4

theorem pred_lt_iff_of_not_isMin (ha : ¬IsMin a) : pred a < b ↔ a ≤ b :=
  ⟨le_of_pred_lt, (pred_lt_of_not_isMin ha).trans_le⟩

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

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

Разделы

Аффилиация

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