This operator can be called with 1 or 3 arguments.
Called with 1 argument, Minimum(S), rendered min(S), represents the minimum element of the set S. This operator is only defined if S
is a subset of R∪{−∞,+∞}
and the minimum exists.
Called with 3 arguments, Minimum(f(x), x, P(x)), rendered P(x)minf(x), represents min({f(x):P(x)}).
The argument 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 x∈S
where S
is a known set. More generally, x can be a collection of variables (x,y,…)
all of which become locally bound, with a corresponding predicate P(x,y,…).
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Minimum | P(x)minf(x) | Minimum value of a set or function |
RR | R | Real numbers |
Infinity | ∞ | Positive infinity |
SetBuilder | {f(x):P(x)} | Set comprehension |
Source code for this entry:
Entry(ID("d0cb24"), SymbolDefinition(Minimum, Minimum(f(x), x, P(x)), "Minimum value of a set or function"), Description("This operator can be called with 1 or 3 arguments."), Description("Called with 1 argument, ", SourceForm(Minimum(S)), ", rendered", Minimum(S), ", represents the minimum element of the set", S, ".", "This operator is only defined if", S, "is a subset of", Union(RR, Set(Neg(Infinity), Pos(Infinity))), " and the minimum exists."), Description("Called with 3 arguments, ", SourceForm(Minimum(f(x), x, P(x))), ", rendered", Minimum(f(x), x, P(x)), ", represents", Minimum(SetBuilder(f(x), x, 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), "."))