succ_coe_of_not_isMax — Mathlib

English

If a is not maximal, then the successor of its embedding in WithTop α equals the embedding of the successor of a.

Русский

Если a не максимален, то следующего элемента после его вложения в WithTop α равен вложению successor(a).

LaTeX

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

Lean4

theorem succ_coe_of_not_isMax {a : α} (h : ¬IsMax a) : succ (↑a : WithTop α) = ↑(succ a) :=
  dif_neg (succ_eq_iff_isMax.not.2 h)

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