pred_coe

Mathlib.Order.SuccPred.Basic

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

English

Under NoMinOrder α, pred(↑a) = ↑(pred a).

Русский

При NoMinOrder α выполняется pred(↑a) = ↑(pred a).

LaTeX

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

Lean4

theorem pred_coe [NoMinOrder α] {a : α} : pred (↑a : WithBot α) = ↑(pred a) :=
  pred_coe_of_not_isMin <| not_isMin a

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

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

Разделы

Аффилиация

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