orderPred_coe

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#WithTop.orderPred_coe

← MathLib Explorer

English

Pred of the embedded element equals embedding of pred.

Русский

Pred(↑a) = ↑(pred a).

LaTeX

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

Lean4

/-- Not to be confused with `WithTop.pred_coe`, which is about `WithTop.pred`. -/
@[simp]
theorem orderPred_coe (a : α) : pred (↑a : WithTop α) = ↑(pred a) :=
  rfl

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

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

Разделы

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

Аффилиация

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