TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

The measure of a set liminf is at most the liminf of the measures

Statement

For every sequence $(E_{k})$ of measurable sets,

$μ ({lim inf}_{k \to \infty} E_{k}) \leq {lim inf}_{k \to \infty} μ (E_{k}),$

where the numerical liminf is taken in $[0, + \infty]$ as in Limit superior and limit inferior of a nonnegative extended-real sequence.

Facts & Assumptions

Given: A measure $μ$ and a sequence $(E_{k})$ of measurable sets.

[L1]

For increasing measurable sets, the measure of the union is the supremum of their measures (Continuity from below for measures).

[L2]

Measures are monotone under inclusion (Measures are monotone).

[L3]

The set liminf is $⋃_{N} ⋂_{k \geq N} E_{k}$ (Limit superior and limit inferior of a sequence of sets).

[L4]

For a nonnegative extended sequence $(a_{k})$ , ${lim inf}_{k} a_{k} = \sup_{N} \inf_{k \geq N} a_{k}$ (Limit superior and limit inferior of a nonnegative extended-real sequence), and all these bounds exist (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$ ).

Proof

technique · direct

1.1givenL3

Put $F_{N} : = ⋂_{k \geq N} E_{k}$ . Then $F_{N} \subseteq F_{N + 1}$ and $⋃_{N} F_{N} = {lim inf}_{k} E_{k}$ .

1.2givenL2L4

For every $N$ and every $k \geq N$ , $F_{N} \subseteq E_{k}$ , so $μ (F_{N}) \leq μ (E_{k})$ and hence $μ (F_{N}) \leq \inf_{k \geq N} μ (E_{k})$ .

2.1step 1.1step 1.2L1L4∎

Continuity from below and step 1.2 give $μ ({lim inf}_{k} E_{k}) = \sup_{N} μ (F_{N}) \leq \sup_{N} \inf_{k \geq N} μ (E_{k}) = {lim inf}_{k} μ (E_{k})$ .

Depends on

Used by

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

Dependency tree · two levels

16 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

G. Folland, Real Analysis, 2nd ed., §1.3, Exercise 8 (standard reference, not scraped)