pred_eq_iff_isMin

Mathlib.Order.SuccPred.Basic

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

English

pred a = a iff a is minimal.

Русский

pred a = a тогда и только тогда, когда a минимален.

LaTeX

$$$$pred(a) = a \iff IsMin(a).$$$$

Lean4

@[simp]
theorem pred_eq_iff_isMin : pred a = a ↔ IsMin a :=
  ⟨fun h => min_of_le_pred h.ge, fun h => h.eq_of_le <| pred_le _⟩

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

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

Разделы

Аффилиация

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