English
Let l be a nonempty finite sequence of elements of α that forms a chain with respect to r. Then the r-series constructed from l by fromListIsChain has toList equal to the original list l.
Русский
Пусть l — ненулевой конечный список элементов множества α, образующий цепочку относительно отношения r. Тогда серия RelSeries, полученная как fromListIsChain l, l_ne_nil hl, имеет toList равный исходному списку l.
LaTeX
$$$ \\operatorname{toList}(\\operatorname{fromListIsChain}(l, l \\neq [], hl)) = l $$$
Lean4
@[simp]
theorem toList_fromListIsChain (l : List α) (l_ne_nil : l ≠ []) (hl : l.IsChain (· ~[r] ·)) :
(fromListIsChain l l_ne_nil hl).toList = l :=
Subtype.ext_iff.mp <| RelSeries.Equiv.right_inv ⟨l, ⟨l_ne_nil, hl⟩⟩
