Fungrim home page

Fungrim entry: 6fe5c1

Symbol: RealLimit limxaf(x)\lim_{x \to a} f(x) Limiting value, real variable
This operator can be called with three or four arguments.
RealLimit(f(x), For(x, a)), rendered as limxaf(x)\lim_{x \to a} f(x), is equivalent to Limit(f(x), For(x, a), Element(x, RR)) but renders to LaTeX without displaying the predicate xRx \in \mathbb{R} which readers will typically understand from context.
RealLimit(f(x), For(x, a), P(x)), rendered as limxa,P(x)f(x)\lim_{x \to a,\,P(x)} f(x), is equivalent to Limit(f(x), For(x, a), And(Element(x, RR), P(x))).
The expression For(x, a) declares x as a locally bound variable within the scope of the arguments to this operator.
Definitions:
Fungrim symbol Notation Short description
RealLimitlimxaf(x)\lim_{x \to a} f(x) Limiting value, real variable
Limitlimxaf(x)\lim_{x \to a} f(x) Limiting value
RRR\mathbb{R} Real numbers
Source code for this entry:
Entry(ID("6fe5c1"),
    SymbolDefinition(RealLimit, RealLimit(f(x), For(x, a)), "Limiting value, real variable"),
    Description("This operator can be called with three or four arguments."),
    Description(SourceForm(RealLimit(f(x), For(x, a))), ", rendered as", RealLimit(f(x), For(x, a)), ", is equivalent to", SourceForm(Limit(f(x), For(x, a), Element(x, RR))), "but renders to LaTeX without displaying the predicate", Element(x, RR), " which readers will typically understand from context."),
    Description(SourceForm(RealLimit(f(x), For(x, a), P(x))), ", rendered as", RealLimit(f(x), For(x, a), P(x)), ", is equivalent to", SourceForm(Limit(f(x), For(x, a), And(Element(x, RR), P(x)))), "."),
    Description("The expression", SourceForm(For(x, a)), "declares", SourceForm(x), "as a locally bound variable within the scope of the arguments to this operator."))

Topics using this entry

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

2020-08-27 09:56:25.682319 UTC