succ_coe — Mathlib

English

If there is no maximum element in α, then the same relation holds globally: succ(↑a) = ↑(succ(a)).

Русский

Если в α нет максимума, то для любого элемента выполняется succ(↑a) = ↑(succ(a)).

LaTeX

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

Lean4

@[simp]
theorem succ_coe [NoMaxOrder α] {a : α} : succ (↑a : WithTop α) = ↑(succ a) :=
  succ_coe_of_not_isMax <| not_isMax a

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