Measurability criterion inside a finite measurable hull (source code)

= Measurability criterion inside a finite measurable hull
{title2=$A\subseteq M,\quad\mu^*(M)<\infty:\quad A\text{ measurable}\iff\mu^*(A)+\mu^*(M\setminus A)=\mu^*(M)$}

For a <regular outer measure> and measurable $M$, the forward implication is <countable additivity>. For the reverse, choose a measurable hull of $A$ and intersect it with $M$ to obtain $A\subseteq B\subseteq M$ and $\mu(B)=\mu^*(A)$. <Measurability> of $B$ splits $M\setminus A$ into $M\setminus B$ and $B\setminus A$, so
$$
\mu^*(M\setminus A)=\mu(M\setminus B)+\mu^*(B\setminus A).
$$
The assumed equality and finiteness force $\mu^*(B\setminus A)=0$. Every outer-<measure>-null <set> is measurable by <Caratheodory measurability criterion>, so $A=B\setminus(B\setminus A)$ is measurable. Finiteness prevents invalid subtraction of infinite masses.