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.
FALSE: a function with a limit at is bounded on its whole domain
Statement
False claim: let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and let have a limit at (The - limit of at a limit point of ). Then is bounded on , that is, the image is a bounded subset of (Lower bound, bounded below, bounded set).
What is true is the local statement, If has a finite limit at then is bounded on some punctured neighbourhood of : there is a radius such that is bounded on . The radius is produced by the limit condition at the single tolerance , and it carries no information whatever about the values of far from , which the limit condition never constrains.
The witness below is on at the point : the limit there is , and is bounded near , while on the whole domain takes values above every real.
Facts & Assumptions
Given: The set (Intervals of : the nine order-convex forms, nondegeneracy, and length), the point , and the function with .
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 of with satisfies .
Limit point and neighbourhoods (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Absolute value: ; for ; ; ; and for , is equivalent to (Basic properties of the absolute value).
Inverses and order: gives , and gives (Inverses of positives are positive, and reciprocation reverses order); for , inverses being unique (Field); and for , is equivalent to (Sign rules for products and monotonicity of multiplication).
Order arithmetic: , hence and with (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities); of two positive reals the smaller is positive, the order being total (Ordered field).
Archimedean property: for every real there is a natural with , and the canonical naturals satisfy (Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, Complete ordered field (least-upper-bound property)).
Bounded set: is bounded when it has an upper bound and a lower bound; a set with no upper bound is not bounded (Lower bound, bounded below, bounded set).
Refutation
The point lies in and is a limit point of : given a real , let be the smaller of and , so ; then lies in and satisfies .
is well defined on : every has , hence and exists, with .
The limit of at exists and equals . Let be an arbitrary real and let be the smaller of and , so . For with we get , hence by [L4]; and .
The image has no upper bound. Let be an arbitrary real; by [L6] fix a natural with , and note . Then satisfies , so , and . So no real bounds above, and is not bounded.
So has a limit at the limit point of its domain and is unbounded on that domain: the claim is false, while If has a finite limit at then is bounded on some punctured neighbourhood of remains true and gives boundedness on , where indeed by step 2.1.
Remarks
-
The limit hypothesis is entirely local and the conclusion asked for is global, so no argument could bridge them. The witness makes that concrete by putting the unbounded behaviour at the other end of the domain, arbitrarily far from in the only sense available here.
-
The sequential analogue is true, and that contrast is worth noting: a convergent sequence is bounded (Every convergent sequence is bounded), because a sequence has only finitely many terms outside any tail, and finitely many reals are bounded. A function has no such structure: the part of outside a punctured neighbourhood of can be infinite and can carry arbitrary values.
-
A bounded version does hold with an extra hypothesis: if is itself contained in a punctured neighbourhood of on which the limit estimate applies, then local and global boundedness coincide. That is a hypothesis on the domain, not a theorem about limits.
Depends on
- If $f$ has a finite limit at $c$ then $f$ is bounded on some punctured neighbourhood of $c$
- 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}$
- Lower bound, bounded below, bounded set
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Every complete ordered field is Archimedean
- Inverses of positives are positive, and reciprocation reverses order
- Sign rules for products and monotonicity of multiplication
- Basic properties of the absolute value
- Order is preserved by adding a constant and by adding inequalities
- Canonical naturals are positive and strictly increasing
- The multiplicative identity is positive
- Field
- Ordered field
- Complete ordered field (least-upper-bound property)
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 35 results over 13 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)
- Archimedean property (Wikipedia) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)