PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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, the Carathéodory extension dominates every other extension and agrees with it on finite-measure sets

Statement

Assume the Axiom of Countable Choice. Let $μ = μ^{*} ∣_{σ (A_{0})}$ be the Carathéodory extension of a premeasure $μ_{0}$ , and let $ν$ be any measure on $σ (A_{0})$ extending $μ_{0}$ . Then $ν (E) \leq μ (E)$ for every $E \in σ (A_{0})$ , with equality whenever $μ (E) < + \infty$ .

Facts & Assumptions

Given: Countable choice, the premeasure, its induced extension $μ$ , a competing extension $ν$ , and a generated measurable set $E$ .

[L0]

Assuming countable choice, the restriction of the induced outer measure to $σ (A_{0})$ is a measure extending $μ_{0}$ . (Assuming countable choice, a premeasure extends through its induced outer measure)

[L1]

If $(E_{n})$ is an increasing sequence of measurable sets for a measure $μ$ , then $μ (⋃_{n} E_{n}) = \sup_{n} μ (E_{n})$ , with no finiteness hypothesis. (Continuity from below for measures)

[L2]

If $A \subseteq B$ are measurable and $μ (A) < + \infty$ , then $μ (B) = μ (A) + μ (B ∖ A)$ ; if also $μ (B) < + \infty$ , finite subtraction gives $μ (B ∖ A) = μ (B) - μ (A)$ . (Measure of a set difference when the smaller set has finite measure)

[L3]

For every measure $λ$ and every sequence $(E_{k})$ of measurable sets, $λ (⋃_{k} E_{k}) \leq \sum_{k} λ (E_{k})$ . (Finite and countable subadditivity of measures)

Proof

technique · direct

1.1

If $(A_{k})$ is any algebra cover of $E$ , monotonicity and [L3] give $ν (E) \leq ν (⋃_{k} A_{k}) \leq \sum_{k} ν (A_{k}) = \sum_{k} μ_{0} (A_{k})$ . Taking the infimum and using the given identity $μ = μ^{*} ∣_{σ (A_{0})}$ gives $ν (E) \leq μ^{*} (E) = μ (E)$ .

L3givenalgebra

2.1

Countable choice makes $μ$ a measure on $σ (A_{0})$ extending $μ_{0}$ by [L0]. Suppose $μ (E) < + \infty$ and choose an algebra cover $(A_{k})$ of $E$ with finite total cost. For $H = ⋃_{k} A_{k}$ and $H_{n} = ⋃_{k < n} A_{k}$ , both extensions agree on every $H_{n} \in A_{0}$ , so [L1] gives $μ (H) = ν (H)$ ; the finite covering cost makes this common value finite.

step 1.1L0L1choose

3.1

Apply [L2] to $E \subseteq H$ for each measure. Step 1.1 applied to $H ∖ E$ gives $ν (H ∖ E) \leq μ (H ∖ E)$ , so finite subtraction from the common value in step 2.1 gives $μ (E) \leq ν (E)$ ; combined with step 1.1, this proves equality.

step 1.1step 2.1L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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., Theorem 1.14 (standard reference, not scraped)