succ_bot — Mathlib

English

In the WithBot extension of a preorder, the bottom element is a fixed point of the successor map: succ(⊥) = ⊥.

Русский

В расширении WithBot частично упорядоченного множества нижний элемент является фиксированной точкой отображения перехода к следующему элементу: succ(⊥) = ⊥.

LaTeX

$$$$ \operatorname{succ}(\bot_{\mathrm{WithBot}\,\alpha})=\bot_{\mathrm{WithBot}\,\alpha} $$$$

Lean4

/-- Not to be confused with `WithBot.orderSucc_bot`, which is about `Order.succ`. -/
@[simp]
theorem succ_bot : succ (⊥ : WithBot α) = ⊥ :=
  rfl

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