Fungrim home page

Fungrim entry: 6ec976

Symbol: Supremum supP(x)f ⁣(x)\mathop{\operatorname{sup}}\limits_{P\left(x\right)} f\!\left(x\right) Supremum of a set or function
This operator can be called with 1 or 3 arguments.
Called with 1 argument, Supremum(S), rendered sup(S)\operatorname{sup}\left(S\right), represents the supremum of the set SS. This operator is only defined if SS is a subset of R{,+}\mathbb{R} \cup \left\{-\infty, +\infty\right\}. The supremum does not need to be an element of SS itself; in particular, for an open interval S=(a,b)S = \left(a, b\right), we have sup(S)=b\operatorname{sup}\left(S\right) = b.
Called with 3 arguments, Supremum(f(x), x, P(x)), rendered supP(x)f ⁣(x)\mathop{\operatorname{sup}}\limits_{P\left(x\right)} f\!\left(x\right), represents sup({f ⁣(x):P ⁣(x)})\operatorname{sup}\left(\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}\right) where P ⁣(x)P\!\left(x\right) is a predicate defining the range of xx.
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
SupremumsupP(x)f ⁣(x)\mathop{\operatorname{sup}}\limits_{P\left(x\right)} f\!\left(x\right) Supremum of a set or function
RRR\mathbb{R} Real numbers
Infinity\infty Positive infinity
OpenInterval(a,b)\left(a, b\right) Open interval
SetBuilder{f ⁣(x):P ⁣(x)}\left\{ f\!\left(x\right) : P\!\left(x\right) \right\} Set comprehension
Source code for this entry:
Entry(ID("6ec976"),
    SymbolDefinition(Supremum, Supremum(f(x), x, P(x)), "Supremum of a set or function"),
    Description("This operator can be called with 1 or 3 arguments."),
    Description("Called with 1 argument, ", SourceForm(Supremum(S)), ", rendered", Supremum(S), ", represents the supremum of the set", S, ".", "This operator is only defined if", S, "is a subset of", Union(RR, Set(Neg(Infinity), Pos(Infinity))), ".", "The supremum does not need to be an element of", S, "itself; in particular, for an open interval", Equal(S, OpenInterval(a, b)), ", we have", Equal(Supremum(S), b), "."),
    Description("Called with 3 arguments, ", SourceForm(Supremum(f(x), x, P(x))), ", rendered", Supremum(f(x), x, P(x)), ", represents", Supremum(SetBuilder(f(x), x, P(x))), "where", P(x), "is a predicate defining the range of", 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-06-18 07:49:59.356594 UTC