toFinset

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#Cycle.toFinset

English

The toFinset function maps a cycle to a finite set, preserving elements.

Русский

Функция toFinset переводит цикл в конечное множество, сохраняя элементы.

LaTeX

$$$\text{toFinset}(s) \;:\; Finset\, \alpha$$$

Lean4

/-- The `s : Cycle α` as a `Finset α`. -/
def toFinset (s : Cycle α) : Finset α :=
  s.toMultiset.toFinset

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

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

Разделы

Аффилиация

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