setOf

Mathlib.Data.Set.Defs

URI: https://scilib.ai/kg/mathlib#setOf

English

The setOf construction turns a predicate into a set: setOf(p) = { x | p(x) }.

Русский

Построение setOf превращает предикат в множество: setOf(p) = { x | p(x) }.

LaTeX

$$$\\mathrm{setOf}(p) = \\{ x : \\alpha \\mid p(x) \\}$$$

Lean4

/-- Turn a predicate `p : α → Prop` into a set, also written as `{x | p x}` -/
def setOf {α : Type u} (p : α → Prop) : Set α :=
  p

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

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

Разделы

Аффилиация

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