Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13
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.

The multiplication rule and finite chain rule for conditional probability

Statement

If P(B)>0, then P(A∩B)=P(A∣B)P(B). More generally, let A0,…,An−1 be events such that P(A0∩⋯∩Ak−1)>0 for every 1≤k<n. Then P ⁣(⋂i<nAi)=P(A0)∏k=1n−1P ⁣(Ak∣⋂i<kAi). For n=0 the intersection and product both have probability or value 1; for n=1 the formula is P(A0)=P(A0).

Facts & Assumptions

Given: Events satisfying the positivity hypotheses in the Statement.

[L1]

For P(B)>0, P(A∣B)=P(A∩B)/P(B) (Conditional probability P(A∣B) for P(B)>0).

Proof

technique · induction
1.1

Multiplying the identity in [L1] by the positive denominator gives P(A∩B)=P(A∣B)P(B).

L1algebra
1.2

For n=0 the empty intersection is Ω and the empty product is 1, while for n=1 the asserted identity is immediate.

basealgebra
1.3

Assume the chain formula holds for n=k≥1, and suppose the stated prefix probabilities are positive for A0,…,Ak.

ih
2.1

Apply step 1.1 to A=Ak and B=⋂i<kAi, then substitute the induction hypothesis for P(B); this gives the chain formula for k+1.

step 1.1step 1.3algebra
3.1

Induction proves the formula for every finite n, and every displayed conditional probability has a positive conditioning event by hypothesis.

step 1.2step 2.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

2 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