ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 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.

Counting premeasure on the finite-cofinite algebra induces counting outer measure

Example

On the finite-cofinite algebra $A_{0}$ of $N$ , let $μ_{0} (A) = ∣ A ∣$ for finite $A$ and $μ_{0} (A) = + \infty$ for cofinite $A$ . Then $μ_{0}$ is a premeasure and its induced outer measure is counting outer measure on every subset of $N$ .

Facts & Assumptions

Given: The finite-cofinite algebra and the function $μ_{0}$ in the Example.

[F1]

A premeasure on an algebra $A_{0}$ vanishes at the empty set and is countably additive whenever a disjoint sequence in $A_{0}$ has its union in $A_{0}$ . (Premeasures on algebras of sets)

[F2]

The set function induced by $μ_{0}$ assigns $E \subseteq X$ the infimum of $\sum_{k} μ_{0} (A_{k})$ over all countable algebra covers $E \subseteq ⋃_{k} A_{k}$ . (The outer set function induced by a premeasure)

[L1]

Every countable algebra cover of an algebra set disjointifies inside that set into algebra members subordinate to the original cover. (A countable algebra cover disjointifies inside the covered algebra set)

[L2]

Counting measure is an outer measure on $P (X)$ and every subset of $X$ is Carathéodory measurable. (Counting measure is an outer measure for which every subset is measurable)

Verification

technique · direct

1.1

The function is the restriction of counting measure, so a disjoint sequence whose union lies in the finite-cofinite algebra has cardinality equal to the nonnegative sum of the member cardinalities, both for a finite union and for an infinite union; hence [F1] holds.

F1algebra

1.2

If $E$ is finite, its self-cover gives induced cost at most $∣ E ∣$ , while [L1] applied to any cover of $E$ yields disjoint subordinate pieces whose total cardinality is $∣ E ∣$ , so every cover costs at least $∣ E ∣$ . If $E$ is infinite, a cover containing a cofinite member has infinite cost; a cover by finite members with finite total cardinality has finite union and cannot cover $E$ , so every cover has infinite cost.

F2L1cases

2.1

Step 1.2 gives the value $∣ E ∣$ for finite $E$ and $+ \infty$ for infinite $E$ , exactly the counting outer measure of [L2].

step 1.2L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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., Section 1.4 (standard reference, not scraped)