LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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.

$lim inf x_{k} \leq lim sup x_{k}$ for every real sequence

Statement

For every sequence $(x_{k})$ of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences),

${lim inf}_{k} x_{k} \leq {lim sup}_{k} x_{k}$

in $\overline{R}$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ , The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined). No hypothesis is placed on $(x_{k})$ : both sides exist for every sequence (The tail suprema of any real sequence are nonincreasing in $\overline{R}$ , so the limit superior exists for every sequence) and the inequality holds between them in every case, including those in which one or both sides are $\pm \infty$ .

Facts & Assumptions

Given: A sequence $(x_{k})$ of reals, its tail ranges $T_{n} = {x_{k} : k \geq n}$ , and the extended tail bounds $s_{n} = \sup T_{n}$ , $i_{n} = \inf T_{n}$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ).

[L1]

Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , an upper bound below every upper bound and a lower bound above every lower bound respectively (Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ , Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L2]

Monotonicity of the tail bounds: $s_{m} \leq s_{n}$ and $i_{n} \leq i_{m}$ whenever $n \leq m$ , and $i_{n} \leq s_{n}$ for every $n$ ; both ${lim sup}_{k} x_{k} = \inf {s_{n}}$ and ${lim inf}_{k} x_{k} = \sup {i_{n}}$ exist (The tail suprema of any real sequence are nonincreasing in $\overline{R}$ , so the limit superior exists for every sequence, Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ).

[L3]

The order on $N$ is total (Order on the natural numbers, $\leq$ is a linear order on $N$ ).

[L4]

The order on $\overline{R}$ is transitive (The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined, Partial order and partially ordered set).

Proof

technique · direct

1.1

Let $m, n \in N$ be arbitrary. The order on $N$ is total, so either $m \leq n$ or $n \leq m$ ; let $p$ be whichever of $m$ and $n$ is the larger, so that $m \leq p$ and $n \leq p$ .

givenL3choose

2.1

Monotonicity of the tail bounds gives $i_{m} \leq i_{p}$ and $s_{p} \leq s_{n}$ , and $i_{p} \leq s_{p}$ holds because $T_{p}$ is nonempty; chaining these by transitivity yields $i_{m} \leq s_{n}$ . As $m$ and $n$ were arbitrary, every tail infimum is below every tail supremum.

step 1.1L2L4

3.1

Fix $n \in N$ . By step 2.1 the element $s_{n}$ is an upper bound of the family ${i_{m} : m \in N}$ , and ${lim inf}_{k} x_{k}$ is its least upper bound, so ${lim inf}_{k} x_{k} \leq s_{n}$ .

step 2.1L1L2

4.1

Since $n$ was arbitrary, ${lim inf}_{k} x_{k}$ is a lower bound of the family ${s_{n} : n \in N}$ , and ${lim sup}_{k} x_{k}$ is its greatest lower bound, so ${lim inf}_{k} x_{k} \leq {lim sup}_{k} x_{k}$ .

step 3.1L1L2∎

Remarks

The inequality can be strict, and that is the interesting case. For the alternating sequence the two sides are $- 1$ and $1$ ( $(- 1)^{k}$ has $lim inf = - 1$ and $lim sup = 1$ , so it does not converge ↗). Equality is exactly convergence, in the extended sense: that is A real sequence converges to $L \in R$ iff $lim inf x_{k} = lim sup x_{k} = L$ , and diverges to $\pm \infty$ iff both equal $\pm \infty$ .
What the proof actually uses is that the two families interleave. Each $i_{m}$ is below each $s_{n}$ , not merely below $s_{m}$ , and getting that needs a common index $p$ beyond both, which is where totality of the order on $N$ enters. Without that step one would only know $i_{n} \leq s_{n}$ for each $n$ , which does not by itself compare a supremum of the first family with an infimum of the second.
No completeness of $R$ is used here beyond what is already inside Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ . The argument is pure order theory in a totally ordered set with a least and a greatest element.

Depends on

Used by

Dependency tree · two levels

28 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

Limit superior and limit inferior (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.3 (standard reference, not scraped)

lim inf⁡xk≤lim sup⁡xkliminfxk​≤limsupxk​ for every real sequence