Garrido, Theorem 2.6 (recalled) — a finitely additive measure on a subring of a boolean algebra extends to the whole algebra

For every boolean algebra $\mathcal A$, every subring $\mathcal R$ of it (IsBooleanSubring) and every finitely additive $\mu$ on $\mathcal R$ with values in $[0, \infty]$ (IsFinitelyAdditiveOn R μ), there is a finitely additive $\bar\mu$ on all of $\mathcal A$ (IsFinitelyAdditiveOn Set.univ μbar) that agrees with $\mu$ on $\mathcal R$.

Garrido's Theorem 2.6 (p. 7) opens by recalling this: “Theorem 2.6 (Invariant Extension Theorem). Recall Carathéodory’s Extension Theorem: If $\mathcal R$ is a subring of the boolean algebra $\mathcal A$ and $\mu$ is a measure on $\mathcal R$, then $\mu$ can be extended to a measure $\bar\mu$ on $\mathcal A$. If $G$ is an amenable group of automorphisms of $\mathcal A$ and $\mathcal R$, $\mu$ are $G$-invariant, then $\bar\mu$ can be chosen to be $G$-invariant.” This statement is its first sentence, the finitely additive extension the notes call Carathéodory's Extension Theorem. For the algebra of all subsets of a set and a ring of sets it is the published FinitelyAdditive.exists_extension_of_isSetRing; a general boolean algebra reduces to that case through its Stone representation, which is not formalized here.