Fungrim entry: bbeb35

Symbol: Infimum —

\mathop{\operatorname{inf}}\limits_{P\left(x\right)} f\!\left(x\right)

— Infimum of a set or function

This operator can be called with 1 or 3 arguments.

Called with 1 argument, Infimum(S), rendered

\operatorname{inf}\left(S\right)

, represents the infimum of the set

S

. This operator is only defined if

S

is a subset of

\mathbb{R} \cup \left\{-\infty, +\infty\right\}

. The infimum does not need to be an element of

S

itself; in particular, for an open interval

S = \left(a, b\right)

, we have

\operatorname{inf}\left(S\right) = a

Called with 3 arguments, Infimum(f(x), x, P(x)), rendered

\mathop{\operatorname{inf}}\limits_{P\left(x\right)} f\!\left(x\right)

, represents

\operatorname{inf}\left(\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}\right)

where

P\!\left(x\right)

is a predicate defining the range of

x

The argument x to this operator defines a locally bound variable. The corresponding predicate

P\!\left(x\right)

must define the domain of

x

unambiguously; that is, it must include a statement such as

x \in S

where

S

is a known set. More generally, x can be a collection of variables

\left(x, y, \ldots\right)

all of which become locally bound, with a corresponding predicate

P\!\left(x, y, \ldots\right)

Definitions:

Fungrim symbol	Notation	Short description
`Infimum`	$\mathop{\operatorname{inf}}\limits_{P\left(x\right)} f\!\left(x\right)$	Infimum of a set or function
`RR`	$\mathbb{R}$	Real numbers
`Infinity`	$\infty$	Positive infinity
`OpenInterval`	$\left(a, b\right)$	Open interval
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension

Source code for this entry:

Entry(ID("bbeb35"),
    SymbolDefinition(Infimum, Infimum(f(x), x, P(x)), "Infimum of a set or function"),
    Description("This operator can be called with 1 or 3 arguments."),
    Description("Called with 1 argument, ", SourceForm(Infimum(S)), ", rendered", Infimum(S), ", represents the infimum of the set", S, ".", "This operator is only defined if", S, "is a subset of", Union(RR, Set(Neg(Infinity), Pos(Infinity))), ".", "The infimum does not need to be an element of", S, "itself; in particular, for an open interval", Equal(S, OpenInterval(a, b)), ", we have", Equal(Infimum(S), a), "."),
    Description("Called with 3 arguments, ", SourceForm(Infimum(f(x), x, P(x))), ", rendered", Infimum(f(x), x, P(x)), ", represents", Infimum(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

Operators