nodup_toList

Mathlib.Data.FinEnum

URI: https://scilib.ai/kg/mathlib#FinEnum.nodup_toList

← MathLib Explorer

English

The enumeration toList α has no duplicates for any FinEnum α.

Русский

У перечисления toList α нет повторяющихся элементов для любого FinEnum α.

LaTeX

$$$ \\mathrm{List.Nodup}(\\mathrm{toList}(\\\\alpha)). $$$

Lean4

@[simp]
theorem nodup_toList [FinEnum α] : List.Nodup (toList α) := by simp only [toList];
  apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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