notMem

Mathlib.Data.List.Nodup

URI: https://scilib.ai/kg/mathlib#List.Nodup.notMem

English

If (a :: l) is nodup, then a does not occur in l.

Русский

Если a :: l не содержит повторов, то a не встречается в l.

LaTeX

$$$ (a :: l).Nodup \rightarrow a \notin l $$$

Lean4

theorem notMem (h : (a :: l).Nodup) : a ∉ l :=
  (nodup_cons.1 h).1

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

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

Разделы

Аффилиация

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