Assuming countable choice, the Carathéodory domain is the completion of the sigma-finite extension

Given: Countable choice, a sigma-finite premeasure, its induced outer measure ${\mu }^{\ast }$, its generated extension $\mu$, and the completion of that extension.

If the premeasure is sigma-finite and $E$ is Carathéodory measurable, there is $H\in \sigma ({\mathcal{A}}_0)$ with $E\subseteq H$ and ${\mu }^{\ast }(H\setminus E)=0$. (Under sigma-finiteness, every Carathéodory measurable set differs from a generated measurable hull by a null set)

Assuming countable choice, an outer measure induced by a premeasure is regular, and every set has a measurable hull in $\sigma ({\mathcal{A}}_0)$. (Assuming countable choice, a premeasure-induced outer measure is regular with generated measurable hulls)

The Carathéodory measurable subsets form a sigma-algebra, and the restriction of the outer measure to it is a complete measure. (Carathéodory's theorem: measurable sets form a sigma-algebra carrying a complete measure)

Assume the Axiom of Countable Choice. Let $(X,\mathcal{A},\mu )$ be a measure space, and let $(X,\bar{\mathcal{A}},\bar{\mu })$ be its completion construction. Then $\bar{\mu }$ is a complete measure on $\bar{\mathcal{A}}$ extending $\mu$. It is the unique complete measure on $\bar{\mathcal{A}}$ that extends $\mu$. (Assuming countable choice, every measure space has a unique complete extension to its completion)

Assuming countable choice, the induced outer measure of a premeasure satisfies ${\mathcal{A}}_0\subseteq {\mathcal{M}}_{{\mu }^{\ast }}$ and ${\mu }^{\ast }{\mathrm{\mid }}_{{\mathcal{A}}_0}={\mu }_0$, so its restriction to $\sigma ({\mathcal{A}}_0)$ is a measure extending ${\mu }_0$. (Assuming countable choice, a premeasure extends through its induced outer measure)