head_fromListIsChain — Mathlib

English

If l is a nonempty r-chain, the head of the r-series built from l is exactly the first element of l.

Русский

Пусть l — ненулевая цепь относительно r. Тогда голова серии RelSeries, построенной из l, равна первому элементу l.

LaTeX

$$$ \\operatorname{head}(\\operatorname{fromListIsChain}(l, l \\neq [], hl)) = l.\\text{head}(l \\neq []) $$$

Lean4

@[simp]
theorem head_fromListIsChain (l : List α) (l_ne_nil : l ≠ []) (hl : l.IsChain (· ~[r] ·)) :
    (fromListIsChain l l_ne_nil hl).head = l.head l_ne_nil := by simp [← apply_zero, List.getElem_zero_eq_head]

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