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.1givenL3choose

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$ .

2.1step 1.1L2L4

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.

3.1step 2.1L1L2

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}$ .

4.1step 3.1L1L2∎

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}$ .

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.

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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