Theorem ovnsplit

Description: The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnsplit.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovnsplit.a	$$⊢\phi \to A\subseteq {ℝ}^X$$
Assertion	ovnsplit	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\le \mathrm{voln*}\left(X\right)\left(A\cap B\right){+}_{𝑒}\mathrm{voln*}\left(X\right)\left(A\setminus B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovnsplit.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovnsplit.a	$$⊢\phi \to A\subseteq {ℝ}^X$$
3		inundif	$$⊢\left(A\cap B\right)\cup \left(A\setminus B\right)=A$$
4	3	eqcomi	$$⊢A=\left(A\cap B\right)\cup \left(A\setminus B\right)$$
5	4	fveq2i	$$⊢\mathrm{voln*}\left(X\right)\left(A\right)=\mathrm{voln*}\left(X\right)\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)$$
6	5	a1i	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)=\mathrm{voln*}\left(X\right)\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)$$
7	2	ssinss1d	$$⊢\phi \to A\cap B\subseteq {ℝ}^X$$
8	2	ssdifssd	$$⊢\phi \to A\setminus B\subseteq {ℝ}^X$$
9	1 7 8	ovnsubadd2	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)\le \mathrm{voln*}\left(X\right)\left(A\cap B\right){+}_{𝑒}\mathrm{voln*}\left(X\right)\left(A\setminus B\right)$$
10	6 9	eqbrtrd	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\le \mathrm{voln*}\left(X\right)\left(A\cap B\right){+}_{𝑒}\mathrm{voln*}\left(X\right)\left(A\setminus B\right)$$