nodup_toList

Mathlib.Data.Finset.Dedup

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

English

The set represented by l.toFinset equals the set of elements of l.

Русский

Множество, задаваемое l.toFinset, равно множеству элементов l.

LaTeX

$$$(l.toFinset : Set\\,\\alpha) = \\{ a \\mid a \\in l \\}$$$

Lean4

theorem nodup_toList (s : Finset α) : s.toList.Nodup :=
  by
  rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
  exact s.nodup

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

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

Разделы

Аффилиация

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