English
Let J be a partially ordered type with a SuccOrder, and i an element of Iic j that is not maximal in Iic j. Then the underlying value of the successor of i equals the successor of the underlying value i.1.
Русский
Пусть J — частично упорядоченный тип с порядком следующего, и i принадлежит Iic(j) и не является максимальным в Iic(j). Тогда значение после i в внешнем порядке совпадает с порядковым successor{i.1}.
LaTeX
$$$\\neg \\mathrm{IsMax}(i) \\Rightarrow (\\mathrm{Order.succ}\,i).1 = \\mathrm{Order.succ}\\,i.1$$$
Lean4
theorem coe_succ_of_not_isMax [SuccOrder J] {j : J} {i : Set.Iic j} (hi : ¬IsMax i) :
(Order.succ i).1 = Order.succ i.1 := by
rw [coe_succ_of_mem]
apply Order.succ_le_of_lt
exact lt_of_le_of_ne (α := Set.Iic j) le_top (by simpa using hi)
