orderPred_top — Mathlib

English

In a Preorder with top, pred of the top equals the embedding of the top of the base order.

Русский

В предпорядке с верхним элементом pred верхнего элемента равен вложению верхнего элемента базового порядка.

LaTeX

$$$$ \operatorname{pred}(\\top_{WithTop(\\alpha)}) = \\uparrow(\\top_{\\alpha}). $$$$

Lean4

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

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