Theorem ovnn0val

Description: The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnn0val.1	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovnn0val.2	$$⊢\phi \to X\ne \varnothing$$
	ovnn0val.3	$$⊢\phi \to A\subseteq {ℝ}^X$$
	ovnn0val.4	$$⊢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	ovnn0val	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)=sup\left(M,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovnn0val.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovnn0val.2	$$⊢\phi \to X\ne \varnothing$$
3		ovnn0val.3	$$⊢\phi \to A\subseteq {ℝ}^X$$
4		ovnn0val.4	$$⊢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\}$$
5	1 3 4	ovnval2	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)=if\left(X=\varnothing ,0,sup\left(M,{ℝ}^{*},<\right)\right)$$
6	2	neneqd	$$⊢\phi \to \neg X=\varnothing$$
7	6	iffalsed	$$⊢\phi \to if\left(X=\varnothing ,0,sup\left(M,{ℝ}^{*},<\right)\right)=sup\left(M,{ℝ}^{*},<\right)$$
8	5 7	eqtrd	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)=sup\left(M,{ℝ}^{*},<\right)$$