isMin_iterate_pred_of_eq_of_lt

Mathlib.Order.SuccPred.Basic

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

← MathLib Explorer

English

If pred^n a = pred^m a with n < m, then pred^n a is minimal.

Русский

Если pred^n a = pred^m a и n < m, тогда pred^n a минимален.

LaTeX

$$$ (h_{eq} : pred^{[n]} a = pred^{[m]} a) \to (h_{lt} : n < m) \to IsMin (pred^{[n]} a) $$$

Lean4

theorem isMin_iterate_pred_of_eq_of_lt {n m : ℕ} (h_eq : pred^[n] a = pred^[m] a) (h_lt : n < m) : IsMin (pred^[n] a) :=
  @isMax_iterate_succ_of_eq_of_lt αᵒᵈ _ _ _ _ _ h_eq h_lt

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

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

Разделы

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

Аффилиация

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