toSet

Mathlib.SetTheory.ZFC.PSet

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

English

Convert a pre-set to the ordinary set of pre-sets by taking its elements.

Русский

Преобразовать пред-множество в обычное множество пред-множество, взяв его элементы.

LaTeX

$$$\\text{toSet} : PSet \\to Set PSet \\text{ defined by }{x | x \in u}$$$

Lean4

/-- Convert a pre-set to a `Set` of pre-sets. -/
def toSet (u : PSet.{u}) : Set PSet.{u} :=
  {x | x ∈ u}

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

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

Разделы

Аффилиация

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