LemmaStatement: AI-adaptedProof: 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.

Assuming countable choice, an infinite-measure set in a semifinite measure space has arbitrarily large finite-measure subsets

Statement

Assume the Axiom of Countable Choice. Let $μ$ be semifinite and let $E$ be measurable with $μ (E) = + \infty$ . For every real $R > 0$ there is measurable $F \subseteq E$ such that

$R < μ (F) < + \infty .$

Facts & Assumptions

Given: The Axiom of Countable Choice, a semifinite measure $μ$ , a measurable $E$ with $μ (E) = + \infty$ , and a real $R > 0$ .

[L1]

Semifiniteness means that every measurable set of positive measure contains a measurable subset of positive finite measure (Finite, sigma-finite, and semifinite measures).

[L2]

Countable choice selects one member from every nonempty natural-number-indexed family (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L3]

Measures are continuous from below on increasing measurable sequences (Continuity from below for measures) and countably subadditive (Finite and countable subadditivity of measures).

[L4]

If $A \subseteq B$ , $μ (A) < + \infty$ , and $μ (B) = + \infty$ , then $μ (B ∖ A) = + \infty$ (Measure of a set difference when the smaller set has finite measure).

[L5]

Every subset of $\overline{R}$ has a supremum there (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$ ).

[L6]

For every real $ε > 0$ there is a natural $n \geq 1$ with $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · contradiction

1.1givenL1L5

Let $M : = \sup {μ (F) : F \subseteq E measurable and μ (F) < + \infty}$ . The family is nonempty because it contains $\emptyset$ , and semifiniteness makes $M > 0$ .

2.1givenstep 1.1L5

If $M = + \infty$ , the definition of supremum directly supplies a finite-measure $F \subseteq E$ with $μ (F) > R$ , so only the case $M < + \infty$ can fail the conclusion.

2.2step 1.1L2assume-contrachoose

Suppose for contradiction that $M < + \infty$ . For each $n$ , the family of measurable finite-measure $F \subseteq E$ with $μ (F) > M - 1 / (n + 1)$ is nonempty; [L2] selects one such $F_{n}$ for every $n$ .

3.1step 1.1step 2.2L3L5L6

Put $G_{n} = ⋃_{k < n + 1} F_{k}$ and $G = ⋃_{n} G_{n}$ . Finite subadditivity makes every $G_{n}$ finite-measure, while $μ (G_{n}) \leq M$ by the definition of $M$ and $μ (G_{n}) > M - 1 / (n + 1)$ because $F_{n} \subseteq G_{n}$ ; [L6] shows these lower bounds approach $M$ , and continuity from below gives $μ (G) = M < + \infty$ .

4.1step 3.1L1L4choose

By [L4], $μ (E ∖ G) = + \infty$ . Semifiniteness supplies measurable $H \subseteq E ∖ G$ with $0 < μ (H) < + \infty$ .

5.1step 2.1step 3.1step 4.1discharge-contradiction∎

The disjoint set $G \cup H \subseteq E$ has finite measure $M + μ (H) > M$ , contradicting the definition of $M$ . Hence $M = + \infty$ , and step 2.1 gives the required $F$ .

Depends on

Used by

Assuming countable choice, the semifinite part is a semifinite measure and equals the original measure exactly when it is semifinite Theorem

Dependency tree · two levels

28 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 14 (standard reference, not scraped)