exists_list_nodup_eq

Mathlib.Data.Finset.Dedup

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

← MathLib Explorer

English

Every Finset s of α can be represented by a nodup list l with l.toFinset = s.

Русский

Каждое Finset s над α можно представить списком l без повторов such that l.toFinset = s.

LaTeX

$$$ \exists l : List \alpha, l.\mathrm{Nodup} ∧ l.toFinset = s $$$

Lean4

theorem exists_list_nodup_eq [DecidableEq α] (s : Finset α) : ∃ l : List α, l.Nodup ∧ l.toFinset = s :=
  ⟨s.toList, s.nodup_toList, s.toList_toFinset⟩

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

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

Разделы

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

Аффилиация

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