Called with 3 arguments SetBuilder(f(x), x, P(x)), rendered as {f(x):P(x)}, represents the set of values f(x)
for all x
satisfying the predicate P(x).
The expression Var(x) declares x as a locally bound variable within the scope of the arguments to this operator. The corresponding predicate P(x)
must define the domain of x
unambiguously; that is, it must include a statement such as x∈S
where S
is a known set. More generally, Var(x, y, Ellipsis) defines a collection of variables (x,y,…)
all of which become locally bound, with a corresponding predicate P(x,y,…).
Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| SetBuilder | {f(x):P(x)} | 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 expression", SourceForm(Var(x)), "declares", SourceForm(x), "as a locally bound variable within the scope of the arguments to this operator. ", "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(Var(x, y, Ellipsis)), "defines a collection of variables", Tuple(x, y, Ellipsis), "all of which become locally bound, with a corresponding predicate", P(x, y, Ellipsis), "."))