ExampleConstruction: 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.

The sign function has both one-sided limits at $0$ and no two-sided limit

Example

Define $sgn : R \to R$ by

$sgn (x) : = {\begin{cases} 1 & x > 0, \\ 0 & x = 0, \\ - 1 & x < 0. \end{cases}$

Then $0$ is a limit point of both $(0, \infty)$ and $(- \infty, 0)$ , both one-sided limits at $0$ exist (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)$ ),

$\lim_{x \to 0^{+}} sgn (x) = 1, \lim_{x \to 0^{-}} sgn (x) = - 1,$

and $sgn$ has no limit at $0$ .

This is the standard illustration of If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree: the two one-sided limits both exist, so nothing is missing on either side, yet they disagree, and disagreement is exactly what the theorem converts into the failure of the two-sided limit. Note also that the value $sgn (0) = 0$ is equal to neither one-sided limit, and is irrelevant to all three assertions (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

Facts & Assumptions

Given: The function $sgn : R \to R$ above, with $A : = R$ , $c : = 0$ , $A^{+} = R \cap (0, \infty) = (0, \infty)$ and $A^{-} = R \cap (- \infty, 0) = (- \infty, 0)$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[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} f (x) = P$ means that for every real $ε > 0$ there is a real $δ > 0$ such that every $x$ in the domain with $0 < ∣ x - c ∣ < δ$ satisfies $∣ f (x) - P ∣ < ε$ .

[L2]

One-sided limits are the limits at $c$ of the restrictions of $f$ to $A^{-}$ and $A^{+}$ , and are well posed exactly when $c$ is a limit point of the set in question (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)$ ).

[L3]

Limit point and neighbourhoods (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L4]

Absolute value: $∣ 0 ∣ = 0$ ; $∣ u ∣ \geq 0$ ; $∣ u ∣ = u$ for $u \geq 0$ and $∣ u ∣ = - u$ for $u \leq 0$ (Basic properties of the absolute value).

[L5]

Order in $R$ : trichotomy, so every real satisfies exactly one of $x > 0$ , $x = 0$ , $x < 0$ ; $0 < 1$ and hence $2 > 0$ , $ε / 2 > 0$ and $ε / 2 < ε$ for $ε > 0$ ; and $1 - (- 1) = 1 + 1 > 0$ , so $- 1 < 1$ and in particular $1 \neq - 1$ (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Ordered field).

[L6]

Two-sided versus one-sided: if $c$ is a limit point of both $A^{-}$ and $A^{+}$ and $\lim_{x \to c} f (x) = L$ , then $\lim_{x \to c^{-}} f (x) = L$ and $\lim_{x \to c^{+}} f (x) = L$ (If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree).

[L7]

At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); applied to the restrictions, each one-sided limit is a single real.

Verification

technique · direct

1.1

$sgn$ is a well-defined function on $R$ : by trichotomy every real satisfies exactly one of the three defining conditions.

1.2

$0$ is a limit point of $A^{+} = (0, \infty)$ and of $A^{-} = (- \infty, 0)$ : given a real $ε > 0$ , the real $ε / 2$ is positive, hence lies in $A^{+}$ , and satisfies $0 < ∣ ε / 2 - 0 ∣ = ε / 2 < ε$ ; and $- ε / 2$ is negative, hence lies in $A^{-}$ , and satisfies $0 < ∣ - ε / 2 - 0 ∣ = ε / 2 < ε$ .

L3L4L5

1.3

The reals $1$ and $- 1$ are distinct, since $1 - (- 1) = 1 + 1 > 0$ .

2.1

$\lim_{x \to 0^{+}} sgn (x) = 1$ : by [L2] this is the limit at $0$ of the restriction of $sgn$ to $A^{+}$ , which is well posed by step 1.2. Given a real $ε > 0$ , any $δ > 0$ serves, since every $x \in A^{+}$ has $x > 0$ , hence $sgn (x) = 1$ and $∣ sgn (x) - 1 ∣ = ∣ 0 ∣ = 0 < ε$ .

step 1.1step 1.2L1L2L4

2.2

$\lim_{x \to 0^{-}} sgn (x) = - 1$ : identically, every $x \in A^{-}$ has $x < 0$ , hence $sgn (x) = - 1$ and $∣ sgn (x) - (- 1) ∣ = ∣ 0 ∣ = 0 < ε$ for every $ε > 0$ and every $δ > 0$ .

step 1.1step 1.2L1L2L4

3.1

Suppose $sgn$ had a limit at $0$ , say $\lim_{x \to 0} sgn (x) = L$ . Since $0$ is a limit point of both $A^{-}$ and $A^{+}$ by step 1.2, [L6] gives $\lim_{x \to 0^{-}} sgn (x) = L$ and $\lim_{x \to 0^{+}} sgn (x) = L$ ; each one-sided limit is single valued by [L7], so steps 2.1 and 2.2 force $L = 1$ and $L = - 1$ , contradicting step 1.3. Hence $sgn$ has no limit at $0$ .

step 1.3step 2.1step 2.2L6L7∎

Remarks

The failure is not about the value at $0$ . Redefining $sgn (0)$ to be $1$ , or $- 1$ , or anything else changes nothing: The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ never evaluates the function at the point, and the two one-sided limits are computed on sets that exclude $0$ (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)$ ). This is a genuine jump, not a removable defect of the kind FALSE: $\lim_{x \to c} f (x) = f (c)$ whenever both sides exist exhibits.
Away from $0$ the function is locally constant, so it has a limit at every other point of $R$ , equal to its value there: for $c > 0$ take $δ$ to be $c$ itself, and every $x$ with $0 < ∣ x - c ∣ < c$ has $x > 0$ and $sgn (x) = 1 = sgn (c)$ ; symmetrically for $c < 0$ . So the single point $0$ carries the whole phenomenon.
Contrast with the two other failures on this page. Here both one-sided limits exist and differ; for $ψ (1 / x)$ at $0$ ( $ψ (1 / x)$ has no limit at $0$ : two sequences tending to $0$ give values constantly $0$ and constantly $1 / 2$ ) the failure is already one-sided, both witnessing sequences there having positive terms; and for the indicator of $Q$ (The indicator of $Q$ has a limit at no point of $R$ ) the failure occurs at every point at once.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

Sign function (Wikipedia) (standard reference, not scraped)
One-sided limit (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)

The sign function has both one-sided limits at 00 and no two-sided limit