nodupKeys_of_nodupKeys_cons

Mathlib.Data.List.Sigma

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

English

If s :: l has NodupKeys, then l has NodupKeys.

Русский

Если s :: l имеет NodupKeys, то l имеет NodupKeys.

LaTeX

$$$ (s :: l).NodupKeys \\implies l.NodupKeys $$$

Lean4

theorem nodupKeys_of_nodupKeys_cons {s : Sigma β} {l : List (Sigma β)} (h : NodupKeys (s :: l)) : NodupKeys l :=
  (nodupKeys_cons.1 h).2

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

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

Разделы

Аффилиация

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