toSet

Mathlib.SetTheory.ZFC.Basic

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

English

Convert a ZFSet to a Set of ZFSet by collecting its elements.

Русский

Преобразуйте ZFSet в множество ZFSet, собирая элементы.

LaTeX

$$$$ toSet(u) = \{ x \mid x \in u \}. $$$$

Lean4

/-- Convert a ZFC set into a `Set` of ZFC sets -/
def toSet (u : ZFSet.{u}) : Set ZFSet.{u} :=
  {x | x ∈ u}

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

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

Разделы

Аффилиация

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