Alphabeta Math
PropositionStatement: Literature-sourcedProof: 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.

A Dirac set function is a probability measure

Statement

For x0∈X, the Dirac set function δx0 is a probability measure on every sigma-algebra on X.

Facts & Assumptions

Given: A sigma-algebra A on a nonempty set X and a point x0∈X.

[L1]

The Dirac set function has value 1 exactly on the measurable sets containing x0, and value 0 otherwise (The Dirac set function at a point).

[L2]

A probability measure is a measure whose value on the whole space is 1 (Probability measures and probability spaces).

[L3]

A nonnegative extended series is the supremum of its finite partial sums, with the empty sum equal to 0 (Series in the nonnegative extended real line).

Proof

technique · direct
1.1givenL1

One has δx0(∅)=0 and δx0(X)=1.

1.2givenL1L3

If (Ek) is pairwise disjoint, then x0 belongs to at most one Ek. If it belongs to none, both δx0(⋃kEk) and ∑kδx0(Ek) are 0; if it belongs to the unique Er, both are 1.

2.1step 1.1step 1.2L2∎

Step 1.2 proves countable additivity and step 1.1 gives the empty-set and total-mass conditions, so δx0 is a probability measure.

Depends on

Used by

Cited to discharge well-definedness by The Dirac set function at a point.

Dependency tree · two levels

9 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