CorollaryStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

The limit inferior is the least subsequential limit in $\overline{\mathbb{R}}$

Statement

Let $(x_k)$ be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences). Then $\liminf_{k} x_k \in \overline{\operatorname{SL}}(x)$ and $\liminf_{k} x_k \le L$ for every $L \in \overline{\operatorname{SL}}(x)$ (Limit superior and limit inferior of a real sequence as $\inf_n \sup_{k \ge n} x_k$ and $\sup_n \inf_{k \ge n} x_k$ in $\overline{\mathbb{R}}$ , Convergence in $\overline{\mathbb{R}}$ and the extended subsequential limit set: $L \in \overline{\mathbb{R}}$ is an extended subsequential limit when some subsequence converges to $L$ , or diverges to $L = \pm\infty$ ).

So the extended subsequential limit set of any real sequence has a least element as well as a greatest one, and the two are $\liminf_k x_k$ and $\limsup_k x_k$ respectively (The limit superior is itself a subsequential limit in $\overline{\mathbb{R}}$ and is the greatest one). Every extended subsequential limit lies between them.

Facts & Assumptions

Given: A sequence $(x_k)$ of reals, and its reflection $y_k := -x_k$ .

[L1]

Reflection on $\overline{\mathbb{R}}$ : $a \mapsto -a$ satisfies $-(-a) = a$ and $a \le b$ if and only if $-b \le -a$ (The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$ , its order, and the arithmetic that is left undefined).

[L2]

$\limsup_k(-x_k) = -\liminf_k x_k$ ( $\limsup(-x_k) = -\liminf(x_k)$ , with the reflection of $\overline{\mathbb{R}}$ exchanging $\pm\infty$ ).

[L3]

For every real sequence the extended subsequential limit set is nonempty and has greatest element the limit superior (The limit superior is itself a subsequential limit in $\overline{\mathbb{R}}$ and is the greatest one).

[L4]

Convergence in $\overline{\mathbb{R}}$ , subsequences and the set $\overline{\operatorname{SL}}$ (Convergence in $\overline{\mathbb{R}}$ and the extended subsequential limit set: $L \in \overline{\mathbb{R}}$ is an extended subsequential limit when some subsequence converges to $L$ , or diverges to $L = \pm\infty$ , Subsequential limit of a real sequence, and the subsequential limit set, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L5]

Scalar multiples of convergent sequences: $z_j \to z$ in $\mathbb{R}$ implies $c z_j \to c z$ (Algebra of limits: sums, scalar multiples, products and quotients).

[L6]

Divergence to $\pm\infty$ , and order reversal: $z_j > M$ is equivalent to $-z_j < -M$ , and $M$ runs over all reals exactly when $-M$ does (Divergence to $+\infty$ and to $-\infty$ , Order is preserved by adding a constant and by adding inequalities).

[L7]

Limit superior and limit inferior of a real sequence (Limit superior and limit inferior of a real sequence as $\inf_n \sup_{k \ge n} x_k$ and $\sup_n \inf_{k \ge n} x_k$ in $\overline{\mathbb{R}}$ ).

Proof

technique · direct

1.1

Put $y_k := -x_k$ , a sequence of reals; then $-y_k = x_k$ for every $k$ , by the involution property of the reflection.

givenL1L4

1.2

Let $L \in \overline{\mathbb{R}}$ and let $n : \mathbb{N} \to \mathbb{N}$ be strictly increasing with $(x_{n_j})$ converging to $L$ in $\overline{\mathbb{R}}$ .

givenL4

1.3

By [L3] applied to the sequence $(y_k)$ , the set $\overline{\operatorname{SL}}(y)$ is nonempty and has greatest element $N_0 := \limsup_k y_k$ , and $N_0 = -\liminf_k x_k$ by [L2].

givenL2L3L7

2.1

The reflected subsequence $(y_{n_j}) = (-x_{n_j})$ converges to $-L$ in $\overline{\mathbb{R}}$ . If $L$ is real this is the scalar rule with $c = -1$ . If $L = +\infty$ then for every real $M$ there is $J$ with $x_{n_j} > M$ for all $j \ge J$ , hence $y_{n_j} < -M$ for all such $j$ ; since $-M$ runs over all reals as $M$ does, $y_{n_j} \to -\infty = -L$ . If $L = -\infty$ the same argument with the inequalities exchanged gives $y_{n_j} \to +\infty = -L$ .

step 1.2L1L4L5L6

3.1

Hence $L \in \overline{\operatorname{SL}}(x)$ implies $-L \in \overline{\operatorname{SL}}(y)$ , the same index map serving. Applying that implication to the sequence $(y_k)$ , whose reflection is $(x_k)$ , gives conversely that $N \in \overline{\operatorname{SL}}(y)$ implies $-N \in \overline{\operatorname{SL}}(x)$ . So $\overline{\operatorname{SL}}(x) = \{\, -N : N \in \overline{\operatorname{SL}}(y) \,\}$ .

step 2.1step 1.1L1L4

4.1

Therefore $-N_0 \in \overline{\operatorname{SL}}(x)$ , and $-N_0 = -(-\liminf_k x_k) = \liminf_k x_k$ ; and for any $L \in \overline{\operatorname{SL}}(x)$ the element $-L$ lies in $\overline{\operatorname{SL}}(y)$ , so $-L \le N_0$ by maximality, whence $\liminf_k x_k = -N_0 \le L$ by order reversal. Thus $\liminf_k x_k$ is the least element of $\overline{\operatorname{SL}}(x)$ .

step 3.1step 1.3L1L2∎

Remarks

Nothing is reconstructed. The subsequence realising $\liminf_k x_k$ is the one produced by The limit superior is itself a subsequential limit in $\overline{\mathbb{R}}$ and is the greatest one for the reflected sequence, read back through $y \mapsto -y$ . That is the whole point of proving $\limsup(-x_k) = -\liminf(x_k)$ , with the reflection of $\overline{\mathbb{R}}$ exchanging $\pm\infty$ first: the recursion and the well-ordering argument are done once.
Combined with the greatest element, this brackets every subsequential limit. For any real sequence and any $L \in \overline{\operatorname{SL}}(x)$ , $\liminf_{k} x_k \;\le\; L \;\le\; \limsup_{k} x_k,$ which contains $\liminf x_k \le \limsup x_k$ for every real sequence as the special case obtained by taking for $L$ either endpoint, both of which are in the set.
The real subsequential limit set inherits the statement only when the value is finite. If $\liminf_k x_k$ is a real number it is the least element of $\operatorname{SL}(x)$ as well, since the two sets agree on $\mathbb{R}$ (Convergence in $\overline{\mathbb{R}}$ and the extended subsequential limit set: $L \in \overline{\mathbb{R}}$ is an extended subsequential limit when some subsequence converges to $L$ , or diverges to $L = \pm\infty$ ). If it is $-\infty$ , then $\operatorname{SL}(x)$ may have no least element at all, or be empty.

Depends on

Used by

The block sequence 1/1; 1/2, 2/2; 1/3, 2/3, 3/3; … has subsequential limit set exactly [0,1] Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 83 results over 29 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Limit superior and limit inferior (Wikipedia) (standard reference, not scraped)
Subsequential limit (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (3.17) (standard reference, not scraped)
N. Donaldson, Math 140A: Real Analysis notes (standard reference, not scraped)

The limit inferior is the least subsequential limit in R‾\overline{\mathbb{R}}R