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.
L'Hôpital's rule for the form at finite or infinite, one-sided endpoints
Statement
Let and let be differentiable on a deleted one-sided or two-sided neighbourhood of , with there. Suppose , as in the chosen mode. If , then in the same mode. The analogous statement at or follows after the substitution , wherever the transformed functions are defined.
Facts & Assumptions
Given: The hypotheses and one fixed approach mode.
Differentiability implies continuity, and the Cauchy quotient lemma gives a point between two arguments at which a secant quotient equals a derivative quotient (A function differentiable at is continuous at , Cauchy's mean-value theorem in quotient form when the denominator derivative is nonzero).
Finite and infinite function limits have the quantified meanings in The - limit of at a limit point of , The left and right limits of at , as limits of the restrictions of to and , Limits at and , and infinite limits at a point, and The extended real line , its order, and the arithmetic that is left undefined.
Composition with is licensed by the chain rule, and ordinary finite limits obey their algebra laws (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with , Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero, Sums, scalar multiples, products and quotients: , , , and when ).
Proof
Extend to by . Their continuity at follows from the assumed zero limits, while differentiability gives continuity at every other point of the segment. For sufficiently close, the quotient lemma on the segment with endpoints gives , where lies strictly between and .
As in the chosen mode, in that mode. Applying the defining finite or infinite limit inequality to the derivative quotient therefore gives .
At infinity, put , . Then , since the common factor cancels. Apply steps 1.1 and 2.1 as or , and translate back.
Depends on
- Cauchy's mean-value theorem in quotient form when the denominator derivative is nonzero
- A function differentiable at $c$ is continuous at $c$
- The left and right limits of $f$ at $c$, as limits of the restrictions of $f$ to $A \cap (-\infty, c)$ and $A \cap (c, \infty)$
- Limits at $+\infty$ and $-\infty$, and infinite limits at a point
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero
- The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 74 results over 22 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, Taylor's theorem and related calculus (standard reference, not scraped)
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 lecture notes (standard reference, not scraped)
- UC Davis, L'Hopital's rule (standard reference, not scraped)
- Colgate University MATH 323, Chapter 5 notes (standard reference, not scraped)