CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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.

Measures converge for a convergent sequence of sets contained in one finite-measure set

Statement

Let $(E_{n})$ and $E$ be measurable sets. Suppose there is measurable $D$ with $μ (D) < + \infty$ and $E_{n} \subseteq D$ for every $n$ , and suppose membership converges pointwise to membership in $E$ : for every $x$ there is $N$ such that, for all $n \geq N$ , one has $x \in E_{n}$ if and only if $x \in E$ . Then

${lim inf}_{n} μ (E_{n}) = {lim sup}_{n} μ (E_{n}) = μ (E) .$

In particular the real sequence $μ (E_{n})$ converges to $μ (E)$ .

Facts & Assumptions

Given: Measurable $E_{n}, E, D$ with $E_{n} \subseteq D$ , $μ (D) < + \infty$ , and pointwise convergence of memberships to $E$ .

[L1]

For a sequence of sets, eventual membership characterizes the set liminf and repeated membership characterizes the set limsup (Set liminf means eventual membership, set limsup means repeated membership, and liminf is contained in limsup).

[L2]

One has $μ (lim inf E_{n}) \leq lim inf μ (E_{n})$ (The measure of a set liminf is at most the liminf of the measures).

[L3]

If the union has finite measure, then $lim sup μ (E_{n}) \leq μ (lim sup E_{n})$ (The limsup of the measures is at most the measure of the set limsup under a finite-union bound).

[L4]

The numerical liminf and limsup are the supremum of tail infima and the infimum of tail suprema, respectively (Limit superior and limit inferior of a nonnegative extended-real sequence).

Proof

technique · direct

1.1

The membership hypothesis and [L1] give ${lim inf}_{n} E_{n} = E = {lim sup}_{n} E_{n}$ .

givenL1

1.2

Since every $E_{n} \subseteq D$ , their union is contained in $D$ and has finite measure. Moreover $E \subseteq D$ : every $x \in E$ belongs to $E_{n}$ for all sufficiently large $n$ , and hence belongs to $D$ .

given

2.1

Apply [L2] and [L3] using steps 1.1 and 1.2 to obtain $μ (E) \leq {lim inf}_{n} μ (E_{n}) \leq {lim sup}_{n} μ (E_{n}) \leq μ (E)$ .

step 1.1step 1.2L2L3L4

3.1

All quantities in step 2.1 are therefore equal; they are finite because $E \subseteq D$ , so the usual squeeze criterion gives real convergence to $μ (E)$ .

step 1.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

T. Tao, An Introduction to Measure Theory, Exercise 1.4.24 (standard reference, not scraped)