succ_coe_of_isMax — Mathlib

English

Let α be a partially ordered set with a successor operation. If a is a maximal element of α, then the successor of its embedded copy in WithTop α is the top element of WithTop α.

Русский

Пусть α упорядочено частично и задана операция successor. Если a является максимальным элементом α, то successor его копии в WithTop α равен верхнему элементу WithTop α.

LaTeX

$$$\\forall a \,:\\alpha, \\operatorname{IsMax}(a) \\rightarrow \\operatorname{succ}(\\iota(a)) = \top_{WithTop(\\alpha)}.$$$

Lean4

@[simp]
theorem succ_coe_of_isMax {a : α} (h : IsMax a) : succ ↑a = (⊤ : WithTop α) :=
  dif_pos (succ_eq_iff_isMax.2 h)

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