False statementConstruction: AI-adaptedVerification: AI-generatedprecheck 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.

FALSE: $f < g$ near $c$ implies $\lim f < \lim g$

Statement

False claim: let $A \subseteq R$ , let $c$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ), let $f, g : A \to R$ have limits at $c$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ), and suppose there is a real $η > 0$ with

$f (x) < g (x) for every x \in A with 0 < ∣ x - c ∣ < η .$

Then $\lim_{x \to c} f (x) < \lim_{x \to c} g (x)$ .

What is true is the non-strict version, If $f \leq g$ on a punctured neighbourhood of $c$ then $\lim f \leq \lim g$ , non-strictly: the hypothesis $f \leq g$ near $c$ gives $\lim f \leq \lim g$ , and that conclusion cannot be improved even when the hypothesis is strengthened to a strict inequality at every point.

Why the strengthening fails. Strictness at each point is not a uniform statement: it says $g (x) - f (x) > 0$ for every $x$ near $c$ , with no lower bound on that positive quantity. The limit only sees the limit of $g - f$ , and a function that is positive everywhere may have limit $0$ . What does survive is the uniform version: if $g (x) - f (x) \geq κ$ near $c$ for a fixed real $κ > 0$ , then $\lim g - \lim f \geq κ > 0$ , by applying If $f \leq g$ on a punctured neighbourhood of $c$ then $\lim f \leq \lim g$ , non-strictly to $f + κ$ and $g$ .

Facts & Assumptions

Given: The set $A : = R$ , the point $c : = 0$ , the constant function $f : R \to R$ with $f (x) : = 0$ for every $x$ , and the function $g : R \to R$ with $g (x) : = ∣ x ∣$ .

[L1]

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

[L2]

Every real is a limit point of $R$ , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L3]

Absolute value: $∣ u ∣ \geq 0$ ; $∣ u ∣ = 0$ exactly when $u = 0$ ; and $∣ u ∣ = u$ for $u \geq 0$ , so $∣ ∣ x ∣ - 0 ∣ = ∣ x ∣$ (Basic properties of the absolute value).

[L4]

Order in $R$ : trichotomy, so $∣ u ∣ \geq 0$ together with $∣ u ∣ \neq 0$ gives $∣ u ∣ > 0$ , and $t < t$ is impossible (Ordered field).

Refutation

technique · direct

1.1

The point $0$ is a limit point of $R$ .

1.2

The strict hypothesis holds with $η : = 1$ : every $x \in R$ with $0 < ∣ x - 0 ∣ < 1$ has $∣ x ∣ \neq 0$ , hence $∣ x ∣ > 0 = f (x)$ , that is $f (x) < g (x)$ .

L3L4

2.1

Both limits exist and are equal to $0$ . For $f$ : $∣ f (x) - 0 ∣ = 0 < ε$ for every $x$ and every real $ε > 0$ , any $δ$ serving. For $g$ : given a real $ε > 0$ take $δ : = ε$ ; every $x$ with $0 < ∣ x - 0 ∣ < δ$ satisfies $∣ ∣ x ∣ - 0 ∣ = ∣ x ∣ < ε$ .

step 1.1L1L3

3.1

So $f (x) < g (x)$ throughout a punctured neighbourhood of $0$ while $\lim_{x \to 0} f (x) = 0 = \lim_{x \to 0} g (x)$ ; the asserted strict inequality $0 < 0$ is impossible by trichotomy, so the claim is false.

step 1.2step 2.1L4∎

Remarks

The non-strict conclusion is sharp, and this witness shows it: the hypothesis is as strong as a pointwise strict inequality can be, and the conclusion still degenerates to equality.
The same phenomenon for sequences is the reason Limits preserve non-strict inequalities is stated non-strictly; the witness there is a positive null sequence compared with the constant $0$ , which is the sequential shadow of the pair above.
A common misuse. From $f < g$ near $c$ one may conclude $\lim f \leq \lim g$ and nothing more; in particular one may not conclude that $\lim g > 0$ from $g > 0$ near $c$ . To get a strict conclusion one needs either a uniform gap, as noted above, or a separate argument such as If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there, which works in the opposite direction: from a nonzero limit to a bound on the values.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §9.3 (standard reference, not scraped)

FALSE: f<gf<g near cc implies lim⁡f<lim⁡glimf<limg