Fungrim entry: cf447f

Symbol: Set —

\left\{\ldots\right\}

— Set with given elements

Set(x, y, z), rendered as

\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

\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

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

Set(f(x), ForElement(x, S)), rendered as

\left\{ f(x) : x \in S \right\}

Set(f(x), ForElement(x, S), P(x)), rendered as

\left\{ f(x) : x \in S \,\mathbin{\operatorname{and}}\, P(x) \right\}

Set(f(x), For(x, a, b)), rendered as

\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

Elementary logic and set theory