TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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, countable covering costs define an outer measure

Statement

Assume the Axiom of Countable Choice. Let $X$ be a set, let $C \subseteq P (X)$ contain $\emptyset$ and $X$ , and let $p : C \to [0, + \infty]$ satisfy $p (\emptyset) = 0$ . For $E \subseteq X$ , define

$μ^{*} (E) : = \inf {\sum_{k = 0}^{\infty} p (C_{k}) : (C_{k})_{k \in N} is in C and E \subseteq ⋃_{k} C_{k}} .$

Then $μ^{*}$ is an outer measure on $X$ . In short: assuming countable choice, the infimum of countable covering costs defines an outer measure.

Facts & Assumptions

Given: The data in the Statement and the Axiom of Countable Choice.

[F1]

Countable choice says that for every family $(X_{n})_{n \in N}$ of nonempty sets, there is a function $f$ on $N$ with $f (n) \in X_{n}$ for every $n$ . (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[L1]

For every double sequence $(a_{i j})_{i, j \in N}$ in $[0, + \infty]$ , the two iterated nonnegative extended sums are equal, so the order of summation may be interchanged even when the common value is $+ \infty$ . (Tonelli's theorem for double series of nonnegative extended real numbers)

[L2]

If $A$ and $B$ are at most countable, then $A \times B$ is at most countable, with an explicit enumeration and no choice principle. (A product of two at most countable sets is at most countable)

Proof

technique · direct

1.1givenalgebra

The sequence consisting only of empty sets covers $\emptyset$ at cost $0$ , so $μ^{*} (\emptyset) = 0$ ; if $E \subseteq F$ , every cover of $F$ covers $E$ , so taking infima gives $μ^{*} (E) \leq μ^{*} (F)$ .

2.1step 1.1F1L1L2choosealgebra∎

Let $(E_{j})$ be a sequence. If some $μ^{*} (E_{j}) = + \infty$ , the desired subadditive inequality is automatic. Otherwise, for $ε > 0$ , [F1] selects for each $j$ a cover $(C_{j k})_{k}$ of $E_{j}$ with cost below $μ^{*} (E_{j}) + ε 2^{- (j + 1)}$ ; [L2] enumerates the doubly indexed family as one sequence covering $⋃_{j} E_{j}$ , and [L1] computes its cost as at most $\sum_{j} μ^{*} (E_{j}) + ε$ , since the displayed geometric error series has partial sums $ε (1 - 2^{- n})$ . Letting $ε$ decrease to $0$ proves countable subadditivity, so with step 1.1 the function is an outer measure.

Depends on

Used by

Assuming countable choice, the outer set function induced by a premeasure is an outer measure Corollary

Dependency tree · two levels

25 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., Proposition 1.10 (standard reference, not scraped)