eq_nil_or_concat' — Mathlib

English

For any list l, either l is empty or l is a concatenation L ++ [b] for some L,b.

Русский

Для любого списка l либо он пуст, либо l = L ++ [b] для некоторых L,b.

LaTeX

$$$\\\\forall l:\\\\, \\text{List }\\\\alpha, \\\\text{l = []} \\\\lor \\\\exists L\\, b,\\\\, l = L ++ [b].$$$

Lean4

/-- `eq_nil_or_concat` in simp normal form -/
theorem eq_nil_or_concat' (l : List α) : l = [] ∨ ∃ L b, l = L ++ [b] := by simpa using l.eq_nil_or_concat

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