isChain_toList — Mathlib

English

For every RelSeries x, the list x.toList is a chain with respect to the r-chain relation.

Русский

Для любого RelSeries x список x.toList образует цепь относительно отношения ~[r].

LaTeX

$$$List.IsChain (\\lambda a b. a ~[r] b) x.toList$$$

Lean4

theorem isChain_toList (x : RelSeries r) : x.toList.IsChain (· ~[r] ·) :=
  by
  rw [List.isChain_iff_get]
  intro i h
  convert x.step ⟨i, by simpa [toList] using h⟩ <;> apply List.get_ofFn

Похожие утверждения