Fungrim entry: 66ca58

Symbol: SetBuilder —

\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}

— Set comprehension

Called with 3 arguments SetBuilder(f(x), x, P(x)), rendered as

\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}

, represents the set of values

f\!\left(x\right)

for all

x

satisfying the predicate

P\!\left(x\right)

The argument x to this operator defines a locally bound variable. The corresponding predicate

P\!\left(x\right)

must define the domain of

x

unambiguously; that is, it must include a statement such as

x \in S

where

S

is a known set. More generally, x can be a collection of variables

\left(x, y, \ldots\right)

all of which become locally bound, with a corresponding predicate

P\!\left(x, y, \ldots\right)

Definitions:

Fungrim symbol	Notation	Short description
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension

Source code for this entry:

Entry(ID("66ca58"),
    SymbolDefinition(SetBuilder, SetBuilder(f(x), x, P(x)), "Set comprehension"),
    Description("Called with 3 arguments", SourceForm(SetBuilder(f(x), x, P(x))), ", rendered as", SetBuilder(f(x), x, P(x)), ", represents the set of values", f(x), "for all", x, "satisfying the predicate", P(x), "."),
    Description("The argument", SourceForm(x), "to this operator defines a locally bound variable.", "The corresponding predicate", P(x), "must define the domain of", x, "unambiguously; that is, it must include a statement such as", Element(x, S), "where", S, "is a known set.", "More generally,", SourceForm(x), "can be a collection of variables", Tuple(x, y, Ellipsis), "all of which become locally bound, with a corresponding predicate", P(x, y, Ellipsis), "."))

Topics using this entry

Elementary logic and set theory