nodupKeys_singleton

Mathlib.Data.List.Sigma

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

English

A singleton list [s] has NodupKeys.

Русский

Список из одного элемента [s] имеет NodupKeys.

LaTeX

$$$ \\mathrm{NodupKeys}([s]) $$$

Lean4

theorem nodupKeys_singleton (s : Sigma β) : NodupKeys [s] :=
  nodup_singleton _

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

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

Разделы

Аффилиация

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