eq_cons_of_length_one — Mathlib

English

If a list l has length 1, then l is the singleton list containing its only element, i.e., l = [l.get 0].

Русский

Если длина списка l равна 1, то l является одиночным списком, состоящим из единственного элемента l[0].

LaTeX

$$$\\\\forall l:\\\\, \\text{List }\\\\alpha,\\\\, \\operatorname{length}(l) = 1 \\\\Rightarrow l = [l_0], \\\\text{ где } l_0 = l[0].$$$

Lean4

theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) : l = [l.get ⟨0, by omega⟩] := by
  refine ext_get (by convert h) (by grind)

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