toSet

Mathlib.Data.Finset.Defs

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

English

Convert a finset to a set in the natural way: toSet(s) = {a | a ∈ s}.

Русский

Пусть Finset α преобразуется в множество естественным образом: toSet(s) = {a | a ∈ s}.

LaTeX

$$$ \mathrm{toSet}(s) = \{ a \mid a \in s \} $$$

Lean4

/-- Convert a finset to a set in the natural way. -/
@[coe]
def toSet (s : Finset α) : Set α :=
  {a | a ∈ s}

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

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

Разделы

Аффилиация

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