toList

Mathlib.Data.Finset.Dedup

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

English

For lists, membership in the Finset matches membership in the list.

Русский

Членство в Finset соответствует членству в списке.

LaTeX

$$$\\forall {l : \\mathsf{List}\\,\\alpha} {a : \\alpha},\\; a \\in l.toFinset \\iff a \\in l$$$

Lean4

/-- Produce a list of the elements in the finite set using choice. -/
noncomputable def toList (s : Finset α) : List α :=
  s.1.toList

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

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

Разделы

Аффилиация

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