instAssociativeAppend_mathlib

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.instAssociativeAppend_mathlib

English

For any fixed element a, the operation cons a: List α → List α is injective; i.e., if cons a l1 = cons a l2 then l1 = l2.

Русский

Для фиксированного элемента a операция cons a: List α → List α инъективна; если cons a l1 = cons a l2, то l1 = l2.

LaTeX

$$∀ l1 l2, List.cons a l1 = List.cons a l2 → l1 = l2$$

Lean4

instance : Std.Associative (α := List α) Append.append where assoc := append_assoc

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru