duplicate_cons

Mathlib.Data.List.Duplicate

URI: https://scilib.ai/kg/mathlib#List.Duplicate.duplicate_cons

English

If x is duplicated in a list l (x ∈+ l), then x occurs in l.

Русский

Если x повторяется в списке l (x ∈+ l), то x встречается в l.

LaTeX

$$$$ \text{If } x \in^{+} l, \ \text{x is in } l. $$$$

Lean4

theorem duplicate_cons (h : x ∈+ l) (y : α) : x ∈+ y :: l :=
  Duplicate.cons_duplicate h

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

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

Разделы

Аффилиация

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