Set(x, y, z), rendered as {x,y,z}, represents the finite set containing the given elements (and similarly with any number of argumeents). In particular, Set() or {} is the empty set, and Set(x) or {x}
is a singleton set.
The special expressions For, ForElement define a set comprehension:
Set(f(x), For(x), P(x)), rendered as {f(x):P(x)}.
Set(f(x), ForElement(x, S)), rendered as {f(x):x∈S}.
Set(f(x), ForElement(x, S), P(x)), rendered as {f(x):x∈SandP(x)}.
Set(f(x), For(x, a, b)), rendered as {f(a),f(a+1),…,f(b)}.
Definitions:
| Fungrim symbol | Notation | Short description |
|---|
Source code for this entry:
Entry(ID("cf447f"),
SymbolDefinition(Set, Set(Ellipsis), "Set with given elements"),
Description(SourceForm(Set(x, y, z)), ", rendered as", Set(x, y, z), ", represents the finite set containing the given elements (and similarly with any number of argumeents).", "In particular, ", SourceForm(Set()), "or", Set(), "is the empty set, and", SourceForm(Set(x)), "or", Set(x), "is a singleton set."),
Description("The special expressions", SourceForm(For), ", ", SourceForm(ForElement), "define a set comprehension:"),
Description(SourceForm(Set(f(x), For(x), P(x))), ", rendered as", Set(f(x), For(x), P(x)), "."),
Description(SourceForm(Set(f(x), ForElement(x, S))), ", rendered as", Set(f(x), ForElement(x, S)), "."),
Description(SourceForm(Set(f(x), ForElement(x, S), P(x))), ", rendered as", Set(f(x), ForElement(x, S), P(x)), "."),
Description(SourceForm(Set(f(x), For(x, a, b))), ", rendered as", Set(f(x), For(x, a, b)), "."))