min_of_le_pred

Mathlib.Order.SuccPred.Basic

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

English

If a ≤ pred(a), then a is minimal (IsMin a).

Русский

Если a ≤ pred(a), то a является минимальным.

LaTeX

$$$ a \le pred(a) \Rightarrow IsMin(a) $$$

Lean4

theorem min_of_le_pred {a : α} : a ≤ pred a → IsMin a :=
  PredOrder.min_of_le_pred

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

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

Разделы

Аффилиация

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