le_pred_iff_isMin

Mathlib.Order.SuccPred.Basic

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

English

The statement a ≤ pred(a) is equivalent to a being minimal.

Русский

Утверждение a ≤ pred(a) эквивалентно тому, что a минимально.

LaTeX

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

Lean4

@[simp]
theorem le_pred_iff_isMin : a ≤ pred a ↔ IsMin a :=
  ⟨min_of_le_pred, fun h => h <| pred_le _⟩

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

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

Разделы

Аффилиация

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