instLawfulIdentityAppendNil_mathlib

English

The empty list acts as a two-sided identity for list concatenation: for any list l, l ++ [] = l and [] ++ l = l.

Русский

Пустой список является двусторонним нейтральным элементом для конкатенации списков: для любого списка l выполняется l ++ [] = l и [] ++ l = l.

LaTeX

$$∀ l : List α, l ++ [] = l ∧ [] ++ l = l$$

Lean4

instance : Std.LawfulIdentity (α := List α) Append.append []
    where
  left_id := nil_append
  right_id := append_nil

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