Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 fn:X→R‾ be measurable for every n∈N. Then the functions

sup⁡nfn,inf⁡nfn,lim sup⁡nfn,lim inf⁡nfn

are measurable. The set

{ x:lim⁡nfn(x) exists in R‾ }

is measurable. In particular, if fn→f pointwise, then f is measurable.

Facts & Assumptions

Given: A measurable space (X,A) and measurable functions fn:X→R‾ for n∈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 (fn(x)) satisfy

lim sup⁡nfn(x)=inf⁡nsup⁡k≥nfk(x),lim inf⁡nfn(x)=sup⁡ninf⁡k≥nfk(x),

Proof

technique · direct
1.1L1given

Let s(x):=sup⁡nfn(x) and i(x):=inf⁡nfn(x). Then for every real [L1, given] a, {s>a}=⋃n{fn>a},{i>a}=⋃q∈Q, q>a ⋂n{fn>q}. Since each threshold set on the right is measurable, [L1] gives measurability of s and i.

2.1step 1.1L2

For each n, the tail functions [step 1.1, L2] sn(x):=sup⁡k≥nfk(x) and in(x):=inf⁡k≥nfk(x) are measurable by step 1.1. Applying step 1.1 again to the sequences (sn) and (in) and then using [L2] yields measurability of lim sup⁡nfn and lim inf⁡nfn.

3.1step 2.1L1L2

Let u:=lim sup⁡nfn and v:=lim inf⁡nfn. The equality set [step 2.1, L1, L2] {u=v} is measurable because {u=v}=⋂q∈Q(({u>q}∩{v>q})∪({u≤q}∩{v≤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.

4.1step 2.1step 3.1L2∎

If fn→f pointwise, then [L2] gives [step 2.1, step 3.1, L2] f=lim sup⁡nfn=lim inf⁡nfn. Since step 2.1 has already proved that both limiting functions are measurable, f is measurable.

Depends on

Dependency tree · 2 levels

Sources