Cylinder premeasure from a positive functional (source code)

= Cylinder premeasure from a positive functional
{title2=$\ell(A)=\phi(1_A)$}

A normalized <positive linear functional> on $C(\Omega)$ for <Cantor space> gives a finitely additive set function on the algebra of <clopen sets>. If a countable disjoint union of such sets is itself clopen, <compactness> gives a finite subcover; all other terms are empty. Finite additivity therefore gives the required <countable additivity>, making $\ell$ a <premeasure>. The <Caratheodory extension theorem> produces a unique <Borel probability measure>.