Theorem ovnlerp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnlerp.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovnlerp.n0	$$⊢\phi \to X\ne \varnothing$$
	ovnlerp.a	$$⊢\phi \to A\subseteq {ℝ}^X$$
	ovnlerp.e	$$⊢\phi \to E\in {ℝ}^{+}$$
	ovnlerp.m	$$⊢M=\left\{z\in {ℝ}^{*}|\exists i\in \left({\left({{ℝ}^2}^X\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup _{j\in \mathbb{N}}\underset{k\in X}{⨉}\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\wedge z=\mathrm{sum^}\left(\left(j\in \mathbb{N}⟼\prod _{k\in X}vol\left(\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\right)\right)\right)\right)\right\}$$
Assertion	ovnlerp	$$⊢\phi \to \exists z\in Mz\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$

Proof

Step	Hyp	Ref	Expression
1		ovnlerp.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovnlerp.n0	$$⊢\phi \to X\ne \varnothing$$
3		ovnlerp.a	$$⊢\phi \to A\subseteq {ℝ}^X$$
4		ovnlerp.e	$$⊢\phi \to E\in {ℝ}^{+}$$
5		ovnlerp.m	$$⊢M=\left\{z\in {ℝ}^{*}|\exists i\in \left({\left({{ℝ}^2}^X\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup _{j\in \mathbb{N}}\underset{k\in X}{⨉}\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\wedge z=\mathrm{sum^}\left(\left(j\in \mathbb{N}⟼\prod _{k\in X}vol\left(\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\right)\right)\right)\right)\right\}$$
6		nfv	$$⊢Ⅎx\phi$$
7		ssrab2	$$⊢\left\{z\in {ℝ}^{*}|\exists i\in \left({\left({{ℝ}^2}^X\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup _{j\in \mathbb{N}}\underset{k\in X}{⨉}\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\wedge z=\mathrm{sum^}\left(\left(j\in \mathbb{N}⟼\prod _{k\in X}vol\left(\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\right)\right)\right)\right)\right\}\subseteq {ℝ}^{*}$$
8	5 7	eqsstri	$$⊢M\subseteq {ℝ}^{*}$$
9	8	a1i	$$⊢\phi \to M\subseteq {ℝ}^{*}$$
10	1 3 5	ovnpnfelsup	$$⊢\phi \to \mathrm{+\infty }\in M$$
11	10	ne0d	$$⊢\phi \to M\ne \varnothing$$
12		0red	$$⊢\phi \to 0\in ℝ$$
13	1 3 5	ovnsupge0	$$⊢\phi \to M\subseteq \left[0,\mathrm{+\infty }\right]$$
14		0xr	$$⊢0\in {ℝ}^{*}$$
15	14	a1i	$$⊢\left(M\subseteq \left[0,\mathrm{+\infty }\right]\wedge y\in M\right)\to 0\in {ℝ}^{*}$$
16		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
17	16	a1i	$$⊢\left(M\subseteq \left[0,\mathrm{+\infty }\right]\wedge y\in M\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
18		ssel2	$$⊢\left(M\subseteq \left[0,\mathrm{+\infty }\right]\wedge y\in M\right)\to y\in \left[0,\mathrm{+\infty }\right]$$
19		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge y\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le y$$
20	15 17 18 19	syl3anc	$$⊢\left(M\subseteq \left[0,\mathrm{+\infty }\right]\wedge y\in M\right)\to 0\le y$$
21	20	ralrimiva	$$⊢M\subseteq \left[0,\mathrm{+\infty }\right]\to \forall y\in M0\le y$$
22	13 21	syl	$$⊢\phi \to \forall y\in M0\le y$$
23		breq1	$$⊢x=0\to \left(x\le y\leftrightarrow 0\le y\right)$$
24	23	ralbidv	$$⊢x=0\to \left(\forall y\in Mx\le y\leftrightarrow \forall y\in M0\le y\right)$$
25	24	rspcev	$$⊢\left(0\in ℝ\wedge \forall y\in M0\le y\right)\to \exists x\in ℝ\forall y\in Mx\le y$$
26	12 22 25	syl2anc	$$⊢\phi \to \exists x\in ℝ\forall y\in Mx\le y$$
27	6 9 11 26 4	infrpge	$$⊢\phi \to \exists w\in Mw\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E$$
28		nfv	$$⊢Ⅎw\phi$$
29		simp3	$$⊢\left(\phi \wedge w\in M\wedge w\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E\right)\to w\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E$$
30	1 2 3 5	ovnn0val	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)=inf\left(M,{ℝ}^{*},<\right)$$
31	30	eqcomd	$$⊢\phi \to inf\left(M,{ℝ}^{*},<\right)=\mathrm{voln*}\left(X\right)\left(A\right)$$
32	31	oveq1d	$$⊢\phi \to inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E=\mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
33	32	3ad2ant1	$$⊢\left(\phi \wedge w\in M\wedge w\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E\right)\to inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E=\mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
34	29 33	breqtrd	$$⊢\left(\phi \wedge w\in M\wedge w\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E\right)\to w\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
35	34	3exp	$$⊢\phi \to \left(w\in M\to \left(w\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E\to w\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E\right)\right)$$
36	28 35	reximdai	$$⊢\phi \to \left(\exists w\in Mw\le inf\left(M,{ℝ}^{*},<\right){+}_{𝑒}E\to \exists w\in Mw\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E\right)$$
37	27 36	mpd	$$⊢\phi \to \exists w\in Mw\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}wM$$
39		nfrab1	$$⊢\underset{\_}{Ⅎ}z\left\{z\in {ℝ}^{*}|\exists i\in \left({\left({{ℝ}^2}^X\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup _{j\in \mathbb{N}}\underset{k\in X}{⨉}\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\wedge z=\mathrm{sum^}\left(\left(j\in \mathbb{N}⟼\prod _{k\in X}vol\left(\left(\left[.\right)\circ i\left(j\right)\right)\left(k\right)\right)\right)\right)\right)\right\}$$
40	5 39	nfcxfr	$$⊢\underset{\_}{Ⅎ}zM$$
41		nfv	$$⊢Ⅎzw\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
42		nfv	$$⊢Ⅎwz\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
43		breq1	$$⊢w=z\to \left(w\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E\leftrightarrow z\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E\right)$$
44	38 40 41 42 43	cbvrexfw	$$⊢\exists w\in Mw\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E\leftrightarrow \exists z\in Mz\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$
45	37 44	sylib	$$⊢\phi \to \exists z\in Mz\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}E$$