pred_coe_of_not_isMin

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#WithBot.pred_coe_of_not_isMin

English

If a is not minimal, then pred(↑a) = ↑(pred(a)).

Русский

Если a не минимален, pred(↑a) = ↑(pred(a)).

LaTeX

$$$$ \operatorname{pred}(\\iota(a)) = \\iota(\\operatorname{pred}(a)). $$$$

Lean4

theorem pred_coe_of_not_isMin {a : α} (h : ¬IsMin a) : pred (↑a : WithBot α) = ↑(pred a) :=
  dif_neg (pred_eq_iff_isMin.not.2 h)

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

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

Разделы

Аффилиация

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