isMin_iterate_pred_of_eq_of_ne

Mathlib.Order.SuccPred.Basic

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

← 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_{ne} : n \neq m) \to IsMin (pred^{[n]} a) $$$

Lean4

theorem isMin_iterate_pred_of_eq_of_ne {n m : ℕ} (h_eq : pred^[n] a = pred^[m] a) (h_ne : n ≠ m) : IsMin (pred^[n] a) :=
  @isMax_iterate_succ_of_eq_of_ne αᵒᵈ _ _ _ _ _ h_eq h_ne

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

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

Разделы

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

Аффилиация

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