English
SuccChain r s selects the successor chain of s, if there exists a chain t strictly containing s; otherwise it is s itself.
Русский
SuccChain r s выбирает цепь-продолжение s, если существует цепь t, строго содержащая s; иначе это сама s.
LaTeX
$$$ SuccChain\\ r\\ s = \\begin{cases} h.choose, & \\text{if } \\exists t, IsChain\\ r\\ s \\land SuperChain\\ r\\ s\\ t \\\\ s, & \\text{otherwise} \\end{cases} $$$
Lean4
/-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `SuccChain s`
is one of these chains. Otherwise it is `s`. -/
def SuccChain (r : α → α → Prop) (s : Set α) : Set α :=
if h : ∃ t, IsChain r s ∧ SuperChain r s t then h.choose else s
