Fungrim home page

Fungrim entry: cf447f

Symbol: Set {}\left\{\ldots\right\} Set with given elements
Set(x, y, z), rendered as {x,y,z}\left\{x, y, z\right\}, 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}\left\{x\right\} 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)}\left\{ f(x) : P(x) \right\}.
Set(f(x), ForElement(x, S)), rendered as {f(x):xS}\left\{ f(x) : x \in S \right\}.
Set(f(x), ForElement(x, S), P(x)), rendered as {f(x):xSandP(x)}\left\{ f(x) : x \in S \,\mathbin{\operatorname{and}}\, P(x) \right\}.
Set(f(x), For(x, a, b)), rendered as {f(a),f ⁣(a+1),,f(b)}\left\{f(a), f\!\left(a + 1\right), \ldots, f(b)\right\}.
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)), "."))

Topics using this entry

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

2020-01-31 18:09:28.494564 UTC