nodup

Mathlib.Data.List.Sigma

URI: https://scilib.ai/kg/mathlib#List.NodupKeys.nodup

English

If a list has NodupKeys, then the underlying list is nodup.

Русский

Если список имеет NodupKeys, то сам список является без повторов (nodup).

LaTeX

$$$ l.NodupKeys \\implies l.Nodup $$$

Lean4

@[grind →]
protected theorem nodup {l : List (Sigma β)} : NodupKeys l → Nodup l :=
  Nodup.of_map _

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

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

Разделы

Аффилиация

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