notMem_keys_of_nodupKeys_cons

Mathlib.Data.List.Sigma

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

English

If s :: l has NodupKeys, then the first component of s is not among the keys of l.

Русский

Если s :: l имеет NodupKeys, то первая компонента s не встречается среди ключей l.

LaTeX

$$$ (s :: l).NodupKeys \\implies s.1 \\notin l.keys $$$

Lean4

theorem notMem_keys_of_nodupKeys_cons {s : Sigma β} {l : List (Sigma β)} (h : NodupKeys (s :: l)) : s.1 ∉ l.keys := by
  grind

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

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

Разделы

Аффилиация

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