English
Given a nonempty list x with x.IsChain (· ~[r] ·), RelSeries r is obtained with length x.length - 1 and with toFun/step defined from x.
Русский
Пусть дан ненулевой список x, удовлетворяющий цепному условию для r; тогда RelSeries r строится длиной x.length - 1, с toFun и step определёнными элементами списка.
LaTeX
$$$\\exists p : RelSeries\\ r, p.length = x.length - 1$$$
Lean4
/-- Every nonempty list satisfying the chain condition gives a relation series -/
@[simps]
def fromListIsChain (x : List α) (x_ne_nil : x ≠ []) (hx : x.IsChain (· ~[r] ·)) : RelSeries r
where
length := x.length - 1
toFun i := x[Fin.cast (Nat.succ_pred_eq_of_pos <| List.length_pos_iff.mpr x_ne_nil) i]
step i := List.isChain_iff_get.mp hx i _
