orderSucc_coe — Mathlib

English

The successor of a non-bottom embedded element equals its embedded successor.

Русский

У вложенного элемента не равного нижнему выполняется succ(↑a) = ↑(succ(a)).

LaTeX

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

Lean4

/-- Not to be confused with `WithBot.succ_coe`, which is about `WithBot.succ`. -/
@[simp]
theorem orderSucc_coe (a : α) : succ (↑a : WithBot α) = ↑(succ a) :=
  rfl

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