Alphabeta Math
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.

Continuity from above when one set has finite measure

Statement

Let (En)n∈N be a decreasing sequence of measurable sets for a measure μ. If μ(En0)<+∞ for some n0, then

μ(⋂n∈NEn)=inf⁡n∈Nμ(En).

Facts & Assumptions

Given: Measurable sets E0⊇E1⊇⋯, an index n0 with μ(En0)<+∞, and E=⋂nEn.

[L1]

For increasing measurable An, μ(⋃nAn)=sup⁡nμ(An) (Continuity from below for measures).

[L2]

If A⊆B and μ(A)<+∞, then μ(B)=μ(A)+μ(B∖A), with real subtraction valid when μ(B)<+∞ (Measure of a set difference when the smaller set has finite measure).

Proof

technique · direct
1.1given

For k∈N put Hk:=En0∖En0+k. Then (Hk) increases and ⋃kHk=En0∖E.

1.2givenL2

Every En0+k and E has finite measure by inclusion in En0, and [L2] gives μ(Hk)=μ(En0)−μ(En0+k) and μ(En0∖E)=μ(En0)−μ(E).

2.1step 1.1step 1.2L1L3algebra

Apply continuity from below to (Hk) and substitute step 1.2: taking the supremum of the left differences is the same as subtracting the infimum of the decreasing finite values, so cancellation of the finite number μ(En0) yields μ(E)=inf⁡kμ(En0+k).

3.1step 2.1L3∎

A decreasing sequence has the same infimum as any of its tails, so step 2.1 gives μ(E)=inf⁡nμ(En); this includes E=∅, μ(E)=0, and a sequence that is constant from n0 onward.

Depends on

Used by

Dependency tree · two levels

14 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