Fungrim home page

Fungrim entry: 66ca58

Symbol: SetBuilder {f ⁣(x):P ⁣(x)}\left\{ f\!\left(x\right) : P\!\left(x\right) \right\} Set comprehension
Called with 3 arguments SetBuilder(f(x), x, P(x)), rendered as {f ⁣(x):P ⁣(x)}\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}, represents the set of values f ⁣(x)f\!\left(x\right) for all xx satisfying the predicate P ⁣(x)P\!\left(x\right).
The argument x to this operator defines a locally bound variable. The corresponding predicate P ⁣(x)P\!\left(x\right) must define the domain of xx unambiguously; that is, it must include a statement such as xSx \in S where SS is a known set. More generally, x can be a collection of variables (x,y,)\left(x, y, \ldots\right) all of which become locally bound, with a corresponding predicate P ⁣(x,y,)P\!\left(x, y, \ldots\right).
Definitions:
Fungrim symbol Notation Short description
SetBuilder{f ⁣(x):P ⁣(x)}\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

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2019-09-15 11:00:55.020619 UTC