Metamath Proof Explorer

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	$⊢ φ \to X \in Fin$
		ovnn0val.2	$⊢ φ \to X \neq \emptyset$
		ovnn0val.3	$⊢ φ \to A \subseteq ℝ^{X}$
		ovnn0val.4	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
	Assertion	ovnn0val	$⊢ φ \to voln* (X) (A) = inf (M ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		ovnn0val.1	$⊢ φ \to X \in Fin$
2		ovnn0val.2	$⊢ φ \to X \neq \emptyset$
3		ovnn0val.3	$⊢ φ \to A \subseteq ℝ^{X}$
4		ovnn0val.4	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
5	1 3 4	ovnval2	$⊢ φ \to voln* (X) (A) = if (X = \emptyset, 0, inf (M ℝ^{*} <))$
6	2	neneqd	$⊢ φ \to \neg X = \emptyset$
7	6	iffalsed	$⊢ φ \to if (X = \emptyset, 0, inf (M ℝ^{} <)) = inf (M ℝ^{} <)$
8	5 7	eqtrd	$⊢ φ \to voln* (X) (A) = inf (M ℝ^{*} <)$