TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero

Statement

Let $A \subseteq \mathbb{R}$ , let $c$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ), let $f, g : A \to \mathbb{R}$ and let $\alpha \in \mathbb{R}$ . Suppose the limits of $f$ and of $g$ at $c$ exist, and write $L := \lim_{x \to c} f(x)$ and $M := \lim_{x \to c} g(x)$ (The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ ). Then:

the limit of $f + g$ at $c$ exists, and $\lim_{x \to c} (f + g)(x) \;=\; \lim_{x \to c} f(x) + \lim_{x \to c} g(x) \;=\; L + M ;$
the limit of $\alpha f$ at $c$ exists, and $\lim_{x \to c} (\alpha f)(x) \;=\; \alpha \lim_{x \to c} f(x) \;=\; \alpha L ;$
the limit of $fg$ at $c$ exists, and $\lim_{x \to c} (fg)(x) \;=\; \Bigl(\lim_{x \to c} f(x)\Bigr)\Bigl(\lim_{x \to c} g(x)\Bigr) \;=\; LM ;$
if $M \ne 0$ , then, writing $A_0 := \{\, x \in A : g(x) \ne 0 \,\}$ , the point $c$ is a limit point of $A_0$ , the quotient $f/g$ is defined on $A_0$ by $(f/g)(x) = f(x) / g(x)$ , the limit of $(f/g)|_{A_0}$ at $c$ exists, and $\lim_{x \to c} (f/g)|_{A_0}(x) \;=\; \frac{\lim_{x \to c} f(x)}{\lim_{x \to c} g(x)} \;=\; \frac{L}{M} .$

Each equation asserts two things at once: that the limit on the left exists, and that it has the stated value. Both are proved. The symbols denote by At a limit point of the domain a function has at most one limit.

Everything below is proved directly from $\varepsilon$ and $\delta$ . No sequence is constructed and no choice principle is used, so all four claims are theorems of ZF. Passing through Heine criterion: $\lim_{x \to c} f(x) = L$ iff $f(x_k) \to L$ for every sequence in $A \setminus \{c\}$ converging to $c$ instead would import the countable choice spent in that theorem's converse direction, for no gain; see The sequence-to- $\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$ , and where this library records that cost.

Why the quotient is stated on $A_0$ . The function $f/g$ is simply not defined where $g$ vanishes, and $g$ may well vanish at points of $A$ arbitrarily far from $c$ ; restricting to $A_0$ is therefore forced. That this restriction still has $c$ as a limit point, so that the limit there means anything at all, is the last claim of If $\lim_{x \to c} f(x) = L \ne 0$ then $|f| > |L|/2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L/2 > 0$ there. The sequential analogue Algebra of limits: sums, scalar multiples, products and quotients needs the corresponding hypothesis in the form "the denominator sequence is nonzero at every index".

Facts & Assumptions

Given: A set $A \subseteq \mathbb{R}$ , a limit point $c$ of $A$ , functions $f, g : A \to \mathbb{R}$ , a real $\alpha$ , and reals $L, M$ with $\lim_{x \to c} f(x) = L$ and $\lim_{x \to c} g(x) = M$ ; for claim 4 also $M \ne 0$ and $A_0 := \{\, x \in A : g(x) \ne 0 \,\}$ (The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ , Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ).

[L1]

The limit condition: $\lim_{x \to c} h(x) = P$ means that for every real $\varepsilon > 0$ there is a real $\delta > 0$ such that every $x$ in the domain of $h$ with $0 < |x - c| < \delta$ satisfies $|h(x) - P| < \varepsilon$ (The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ ).

[L2]

Absolute value: $|u| \ge 0$ ; $|u| = 0$ if and only if $u = 0$ ; $|uv| = |u|\,|v|$ ; and $|{-u}| = |u|$ (Basic properties of the absolute value).

[L3]

Triangle inequality: $|u + v| \le |u| + |v|$ (The triangle inequality).

[L4]

Order and field arithmetic in $\mathbb{R}$ : adding two strict inequalities (Order is preserved by adding a constant and by adding inequalities); for $t > 0$ , $u < v$ is equivalent to $ut < vt$ , and $0 \le u \le v$ with $0 \le s \le t$ gives $us \le vt$ (Sign rules for products and monotonicity of multiplication); positive elements have positive inverses and $0 < a < b$ gives $0 < 1/b < 1/a$ (Inverses of positives are positive, and reciprocation reverses order); $0 < 1$ (The multiplicative identity is positive), so $2 > 0$ and $t/2 > 0$ for $t > 0$ ; inverses and the field identities (Field); trichotomy and totality, so of finitely many positive reals the smallest is positive (Ordered field).

[L5]

Local boundedness: there are a real $\delta_0 > 0$ and a real $K \ge 0$ with $|f(x)| \le K$ for every $x \in A$ satisfying $0 < |x - c| < \delta_0$ (If $f$ has a finite limit at $c$ then $f$ is bounded on some punctured neighbourhood of $c$ ).

[L6]

Sign preservation: if $M \ne 0$ there is a real $\delta_s > 0$ with $|g(x)| > |M|/2 > 0$ for every $x \in A$ satisfying $0 < |x - c| < \delta_s$ , and $c$ is a limit point of $A_0$ (If $\lim_{x \to c} f(x) = L \ne 0$ then $|f| > |L|/2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L/2 > 0$ there).

[L7]

Restriction: if $B \subseteq A$ has $c$ as a limit point and $\lim_{x \to c} f(x) = L$ , then $\lim_{x \to c} f|_B(x) = L$ (claim 2 of The limit at $c$ depends only on the restriction of $f$ to a punctured neighbourhood of $c$ , and passes to any subset of the domain having $c$ as a limit point).

[L8]

Neighbourhoods (The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ ).

Proof

technique · direct

1.1

Sum. Let $\varepsilon > 0$ be an arbitrary real. By [L1] fix reals $\delta_1, \delta_2 > 0$ with $|f(x) - L| < \varepsilon/2$ for every $x \in A$ satisfying $0 < |x - c| < \delta_1$ and $|g(x) - M| < \varepsilon/2$ for every $x \in A$ satisfying $0 < |x - c| < \delta_2$ , and let $\delta$ be the smaller of the two, so $\delta > 0$ . For $x \in A$ with $0 < |x - c| < \delta$ we get $|(f+g)(x) - (L+M)| = |(f(x) - L) + (g(x) - M)| \le |f(x) - L| + |g(x) - M| < \varepsilon$ . As $\varepsilon$ was arbitrary, the limit of $f + g$ at $c$ exists and equals $L + M$ : claim 1.

L1L2L3L4choose

1.2

Scalar multiple. If $\alpha = 0$ then $\alpha f$ is the constant function $0$ and $\alpha L = 0$ , so $|(\alpha f)(x) - \alpha L| = 0 < \varepsilon$ for every $x$ and every $\varepsilon > 0$ , any $\delta$ serving. If $\alpha \ne 0$ then $|\alpha| > 0$ ; given a real $\varepsilon > 0$ , [L1] supplies $\delta > 0$ with $|f(x) - L| < \varepsilon/|\alpha|$ on $A \cap N^{*}_{\delta}(c)$ , and there $|(\alpha f)(x) - \alpha L| = |\alpha|\,|f(x) - L| < \varepsilon$ . So the limit of $\alpha f$ at $c$ exists and equals $\alpha L$ : claim 2.

L1L2L4L8choose

1.3

A working bound for $f$ near $c$ . By [L5] fix a real $\delta_0 > 0$ and a real $K \ge 0$ with $|f(x)| \le K$ for every $x \in A$ satisfying $0 < |x - c| < \delta_0$ , and put $K' := K + 1$ , so $K' > 0$ and $|f(x)| \le K'$ for all those $x$ .

L4L5choose

1.4

The denominator near $c$ . Assume $M \ne 0$ . By [L6] fix a real $\delta_s > 0$ with $|g(x)| > |M|/2 > 0$ for every $x \in A$ satisfying $0 < |x - c| < \delta_s$ ; every such $x$ has $g(x) \ne 0$ , hence lies in $A_0$ , and $c$ is a limit point of $A_0$ .

L2L4L6

2.1

Product. Let $\varepsilon > 0$ be an arbitrary real. By [L1] fix reals $\delta_1, \delta_2 > 0$ with $|g(x) - M| < \varepsilon/(2K')$ on $A \cap N^{*}_{\delta_1}(c)$ and $|f(x) - L| < \varepsilon / \bigl(2(|M| + 1)\bigr)$ on $A \cap N^{*}_{\delta_2}(c)$ , and let $\delta$ be the smallest of $\delta_0, \delta_1, \delta_2$ , which is positive. For $x \in A$ with $0 < |x - c| < \delta$ , $|f(x)g(x) - LM| = |f(x)(g(x) - M) + M(f(x) - L)| \le |f(x)|\,|g(x) - M| + |M|\,|f(x) - L| \le K'\,|g(x) - M| + (|M|+1)\,|f(x) - L| < \varepsilon/2 + \varepsilon/2 = \varepsilon$ . As $\varepsilon$ was arbitrary, the limit of $fg$ at $c$ exists and equals $LM$ : claim 3.

step 1.3L1L2L3L4L8choose

2.2

Reciprocal. Assume $M \ne 0$ and let $\varepsilon > 0$ be an arbitrary real. By [L1] fix a real $\delta_3 > 0$ with $|g(x) - M| < \varepsilon |M|^2 / 2$ on $A \cap N^{*}_{\delta_3}(c)$ , and let $\delta$ be the smaller of $\delta_s$ and $\delta_3$ . For $x \in A_0$ with $0 < |x - c| < \delta$ we have $|g(x)| > |M|/2 > 0$ , hence $|g(x)|\,|M| > |M|^2/2 > 0$ and so $1/(|g(x)|\,|M|) < 2/|M|^2$ ; therefore $\bigl| 1/g(x) - 1/M \bigr| = |M - g(x)| \big/ \bigl(|g(x)|\,|M|\bigr) < (\varepsilon |M|^2/2)\cdot(2/|M|^2) = \varepsilon$ . As $\varepsilon$ was arbitrary, the limit of $(1/g)|_{A_0}$ at $c$ exists and equals $1/M$ .

step 1.4L1L2L4L8choose

2.3

The numerator on the smaller domain. Assume $M \ne 0$ . Since $A_0 \subseteq A$ and $c$ is a limit point of $A_0$ by step 1.4, [L7] gives that the limit of $f|_{A_0}$ at $c$ exists and equals $L$ .

step 1.4L7

3.1

Quotient. Assume $M \ne 0$ . On the domain $A_0$ , which has $c$ as a limit point, the two functions $f|_{A_0}$ and $(1/g)|_{A_0}$ have limits $L$ and $1/M$ at $c$ by steps 2.3 and 2.2, and their product is $(f/g)|_{A_0}$ by the field identities; so claim 3, applied on the domain $A_0$ , gives that the limit of $(f/g)|_{A_0}$ at $c$ exists and equals $L \cdot (1/M) = L/M$ .

step 2.1step 2.2step 2.3L2L4

4.1

Claims 1 to 4 are proved, each directly from the $\varepsilon$ - $\delta$ definition and none of them through a sequence.

step 1.1step 1.2step 2.1step 3.1∎

Remarks

The product estimate in one line. The identity $fg - LM = f\,(g - M) + M\,(f - L)$ turns the problem into two products, one with a factor that is merely bounded near $c$ (that is $f$ , and If $f$ has a finite limit at $c$ then $f$ is bounded on some punctured neighbourhood of $c$ is what bounds it) and one with a constant factor. The two constants $K'$ and $|M| + 1$ are used in place of $K$ and $|M|$ only so that they are strictly positive and may be divided by; that is the sole reason for adding $1$ .
The reciprocal estimate in one line. The identity $1/g - 1/M = (M - g)/(gM)$ turns the problem into a numerator that is small and a denominator that must be kept away from $0$ ; the lower bound $|g| > |M|/2$ from If $\lim_{x \to c} f(x) = L \ne 0$ then $|f| > |L|/2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L/2 > 0$ there does exactly that, and gives the working factor $2/|M|^2$ .
Nothing here extends to $\pm\infty$ . The statement is about a finite limit point $c$ and finite values $L, M$ ; Limits at $+\infty$ and $-\infty$ , and infinite limits at a point introduces limits at and to infinity, but no algebra of such limits is proved in this library, and none may be assumed. The companion page's limit at $+\infty$ is computed by a direct estimate for precisely that reason.
The sequential analogue is Algebra of limits: sums, scalar multiples, products and quotients. Neither implies the other for free: this theorem is about a function on a subset of $\mathbb{R}$ and is proved from $\varepsilon$ and $\delta$ ; that one is about sequences.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I, §3.1: Limits of functions (standard reference, not scraped)
Limit of a function (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Thm 4.4) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §9.3 (standard reference, not scraped)