TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-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.

Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable

Statement

Let $(X, A)$ be a measurable space and let $f_{n} : X \to \overline{R}$ be measurable for every $n \in N$ . Then the functions

$\sup_{n} f_{n}, \inf_{n} f_{n}, {lim sup}_{n} f_{n}, {lim inf}_{n} f_{n}$

are measurable. The set

${x : \lim_{n} f_{n} (x) exists in \overline{R}}$

is measurable. In particular, if $f_{n} \to f$ pointwise, then $f$ is measurable.

Facts & Assumptions

Given: A measurable space $(X, A)$ and measurable functions $f_{n} : X \to \overline{R}$ for $n \in N$ .

[L1]

Threshold measurability characterizes extended-real measurability. (Threshold characterisations of real-valued and extended-real-valued measurability)

[L2]

For each $x$ , the limsup and liminf of the sequence $(f_{n} (x))$ satisfy

${lim sup}_{n} f_{n} (x) = \inf_{n} \sup_{k \geq n} f_{k} (x), {lim inf}_{n} f_{n} (x) = \sup_{n} \inf_{k \geq n} f_{k} (x),$

and the pointwise limit exists exactly when the limsup and liminf are equal. (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}$ , 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$ )

Proof

technique · direct

1.1

Let $s (x) : = \sup_{n} f_{n} (x)$ and $i (x) : = \inf_{n} f_{n} (x)$ . Then for every real [L1, given] $a$ ,

${s > a} = ⋃_{n} {f_{n} > a}, {i > a} = ⋃_{q \in Q, q > a} ⋂_{n} {f_{n} > q} .$

Since each threshold set on the right is measurable, [L1] gives measurability of $s$ and $i$ . [L1, given]

2.1

For each $n$ , the tail functions [step 1.1, L2] $s_{n} (x) : = \sup_{k \geq n} f_{k} (x)$ and $i_{n} (x) : = \inf_{k \geq n} f_{k} (x)$ are measurable by step 1.1. Applying step 1.1 again to the sequences $(s_{n})$ and $(i_{n})$ and then using [L2] yields measurability of ${lim sup}_{n} f_{n}$ and ${lim inf}_{n} f_{n}$ .

step 1.1L2

3.1

Let $u : = {lim sup}_{n} f_{n}$ and $v : = {lim inf}_{n} f_{n}$ . The equality set [step 2.1, L1, L2] ${u = v}$ is measurable because

${u = v} = ⋂_{q \in Q} (({u > q} \cap {v > q}) \cup ({u \leq q} \cap {v \leq q})) .$

If $u (x) < v (x)$ or $v (x) < u (x)$ , a rational strictly between them separates the two sides; if $u (x) = v (x)$ , every rational lies on the same side of both values. So [L2] makes the pointwise-convergence set measurable. [step 2.1, L1, L2]

4.1

If $f_{n} \to f$ pointwise, then [L2] gives [step 2.1, step 3.1, L2] $f = {lim sup}_{n} f_{n} = {lim inf}_{n} f_{n}$ . Since step 2.1 has already proved that both limiting functions are measurable, $f$ is measurable.

step 2.1step 3.1L2∎

Depends on

Used by

A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra Theorem

Dependency tree · two levels

27 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

Sheldon Axler, Measure, Integration and Real Analysis, Proposition 2.53 (standard reference, not scraped)