Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Counting measure is a measure

Statement

For every set X, the counting set function #X of Counting measure on an arbitrary set is a measure on (X,P(X)).

Facts & Assumptions

Given: A set X and a pairwise disjoint sequence (Ek) of subsets of X.

[L1]

Counting measure assigns a finite set its finite cardinality and an infinite set the value + (Counting measure on an arbitrary set).

[L2]

A measure must vanish at the empty set and be countably additive on pairwise disjoint measurable sequences (Measures on sigma-algebras).

[L3]

A nonnegative extended series is the supremum of its finite partial sums (Series in the nonnegative extended real line).

[L4]

A set is finite when it is equinumerous with a natural number, and otherwise it may be countably infinite or uncountable (Finite, countably infinite, countable, uncountable).

Proof

technique · direct
1.1

One has #X()=0. For every n, disjointness gives #X(k<nEk)=k<n#X(Ek) whenever all those sets are finite.

givenL1
1.2

If some Er is infinite, then kEk is infinite and both #X(kEk) and k#X(Ek) are +.

givenL1L3
2.1

Suppose every Ek is finite. If E:=kEk is finite, only finitely many pairwise disjoint Ek can be nonempty, and step 1.1 gives #X(E)=k#X(Ek).

givenstep 1.1L1L3L4
2.2

Suppose every Ek is finite but E is infinite. For every mN, the set E contains more than m distinct points; the finitely many indices of the Ek containing those points have a strict upper bound n (take one more than their maximum), so step 1.1 gives k<n#X(Ek)>m. Hence the partial sums are unbounded and their supremum is +=#X(E).

givenstep 1.1L1L3L4
3.1

Steps 1.2, 2.1 and 2.2 cover all possibilities for the union, so countable additivity holds; with #X()=0 from step 1.1, [L2] proves that #X is a measure.

step 1.1step 1.2step 2.1step 2.2L2

Depends on

Used by

Cited to discharge well-definedness by Counting measure on an arbitrary set.

Dependency tree · two levels

13 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