Alphabeta Math

Limits of Real Functions

About this page
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.

✓ 17 results · all verified · 14 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Definition

The ε-δ limit lim_x → c f(x) = L of f : A → ℝ at a limit point c of A

Lemma

At a limit point of the domain a function has at most one limit

Lemma

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

Definition

The left and right limits of f at c, as limits of the restrictions of f to A ∩ (-∞, c) and A ∩ (c, ∞)

Definition

Limits at +∞ and -∞, and infinite limits at a point

Theorem

Heine criterion: lim_x → c f(x) = L iff f(xₖ) → L for every sequence in A ∖ {c} converging to c

Corollary

A function has no limit at c as soon as two sequences in A ∖ {c} tending to c give different limits of the values

Lemma

If f has a finite limit at c then f is bounded on some punctured neighbourhood of c

Lemma

If lim_x → c f(x) = L ≠ 0 then |f| > |L|/2 on a punctured neighbourhood of c; in particular if L > 0 then f > L/2 > 0 there

Theorem

Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero

Lemma

If f ≤ g on a punctured neighbourhood of c then lim f ≤ lim g, non-strictly

Theorem

If f ≤ g ≤ h near c and f and h have the same limit at c, then so does g

Theorem

If c is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree

Theorem

Composition of limits holds under either hypothesis: f is defined at L with value M, or g avoids L on a punctured neighbourhood of c

Lemma

Integer part: for every real x there is exactly one integer m with m ≤ x < m + 1

Remark

The sequence-to-ε direction of the Heine criterion uses countable choice for ℝ, and where this library records that cost

False statement

FALSE: lim_x → c f(x) = f(c) whenever both sides exist

False statement

FALSE: lim_x → c f(g(x)) = M whenever lim_x → c g = L and lim_y → L f = M

False statement

FALSE: a function has at most one limit at every point of its domain, isolated points included

False statement

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

False statement

FALSE: a function with a limit at c is bounded on its whole domain

Sources