English
A construction of a SuccOrder structure starting from a successor function succ and a bijection between x < b and succ a ≤ b.
Русский
Конструкция SuccOrder α из заданной функции продолжения и эквивалентности между отношениями «меньше» и «меньше или равно» после применения succ.
LaTeX
$$$\\text{SuccOrder}(\\alpha) = (\\text{succ}, \\text{le_succ}, \\text{max_of_succ_le}, \\text{succ_le_of_lt})$ with $\\forall a, b,\\ (a < b) \\iff (succ\\ a \\le b)$.$$
Lean4
/-- A constructor for `SuccOrder α` usable when `α` has no maximal element. -/
def ofSuccLeIff (succ : α → α) (hsucc_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b) : SuccOrder α :=
{ succ
le_succ := fun _ => (hsucc_le_iff.1 le_rfl).le
max_of_succ_le := fun ha => (lt_irrefl _ <| hsucc_le_iff.1 ha).elim
succ_le_of_lt := fun h => hsucc_le_iff.2 h }
