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.
The function equal to off the origin and to at the origin has limit there
Statement refuted
Refuted claim: if is a limit point of and has a limit at , then — the false statement FALSE: whenever both sides exist.
The witness is the smallest one available: the function
at the point . It has limit there, while .
Beyond refuting the claim, this item records two further facts about the same witness, both used elsewhere on the page: both one-sided limits at also equal , so the defect is not a jump; and changing the single value to produces a function with the same limit and the equality restored. That is what makes this a removable defect, and it is the pattern the composition counterexample With and equal to off the origin and at it, and while exploits.
Facts & Assumptions
Given: The function above and the point ; and the constant function with for every .
The limit condition (The - limit of at a limit point of ): means that for every real there is a real such that every in the domain with satisfies .
Limit point: every real is a limit point of , punctured neighbourhoods being never empty; and is a limit point of and of , since and lie in them at distance from (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of , Intervals of : the nine order-convex forms, nondegeneracy, and length).
Absolute value: ; exactly when (Basic properties of the absolute value).
Order in : trichotomy, so every real either equals or does not, exclusively; , so , and for (The multiplicative identity is positive, Ordered field).
One-sided limits are the limits of the restrictions to and (The left and right limits of at , as limits of the restrictions of to and ).
Locality: if two functions on agree on for some real , they have the same limits at (claim 1 of The limit at depends only on the restriction of to a punctured neighbourhood of , and passes to any subset of the domain having as a limit point).
Counterexample
is a well-defined function on , by trichotomy; and is a limit point of .
The reals and are distinct.
The limit of at exists and equals : given an arbitrary real , take ; every with has , hence , hence and .
Both one-sided limits of at exist and equal : the point is a limit point of and of by [L2], and every in either set satisfies , hence ; so any serves in the definition of each one-sided limit.
Yet , and : at the point of the domain, which is a limit point of the domain, the limit exists and differs from the value, refuting the claim.
Changing the single value repairs the equality: and the constant function agree at every , hence on , so by [L6] the limit of at exists and equals ; and is that limit.
So the limit at a point of the domain is independent of the value of the function there, and the two agree only under an extra hypothesis on the function, never as a consequence of the limit existing.
Remarks
-
A removable defect, not a jump. By step 2.2 the two one-sided limits exist and agree with each other and with the two-sided limit; the only disagreement is with the value. Compare the sign function (The sign function has both one-sided limits at and no two-sided limit), where the two one-sided limits exist and disagree, and no redefinition of the value can repair anything.
-
Why the witness is used again for composition. Because , hypothesis (i) of Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of fails for at ; feeding it an inner function that takes the value then breaks the composition, which is With and equal to off the origin and at it, and while .
-
Nothing here depends on the particular values and , only on their being distinct. Any function constant off with a different value at refutes the claim in the same three lines.
Depends on
- FALSE: $\lim_{x \to c} f(x) = f(c)$ whenever both sides exist
- 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}$
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
- 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)$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- 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
- Basic properties of the absolute value
- The multiplicative identity is positive
- Ordered field
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 36 results over 15 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)
- Classification of discontinuities (Wikipedia) (standard reference, not scraped)
- Limit of a function (Wikipedia) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)