df-ovoln

Description: Define the outer measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	df-ovoln	$⊢ voln* = (x \in Fin ⟼ (y \in 𝒫 (ℝ^{x}) ⟼ if (x = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\} ℝ^{} <))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		covoln	$class voln*$
1		vx	$setvar x$
2		cfn	$class Fin$
3		vy	$setvar y$
4		cr	$class ℝ$
5		cmap	$class ↑_{𝑚}$
6	1	cv	$setvar x$
7	4 6 5	co	$class (ℝ^{x})$
8	7	cpw	$class 𝒫 (ℝ^{x})$
9		c0	$class \emptyset$
10	6 9	wceq	$wff x = \emptyset$
11		cc0	$class 0$
12		vz	$setvar z$
13		cxr	$class ℝ^{*}$
14		vi	$setvar i$
15	4 4	cxp	$class ℝ^{2}$
16	15 6 5	co	$class ({ℝ^{2}}^{x})$
17		cn	$class ℕ$
18	16 17 5	co	$class ({({ℝ^{2}}^{x})}^{ℕ})$
19	3	cv	$setvar y$
20		vj	$setvar j$
21		vk	$setvar k$
22		cico	$class [.)$
23	14	cv	$setvar i$
24	20	cv	$setvar j$
25	24 23	cfv	$class i (j)$
26	22 25	ccom	$class ([.) \circ i (j))$
27	21	cv	$setvar k$
28	27 26	cfv	$class ([.) \circ i (j)) (k)$
29	21 6 28	cixp	$class \underset{k \in x}{⨉} ([.) \circ i (j)) (k)$
30	20 17 29	ciun	$class ⋃_{j \in ℕ} \underset{k \in x}{⨉} ([.) \circ i (j)) (k)$
31	19 30	wss	$wff y \subseteq ⋃_{j \in ℕ} \underset{k \in x}{⨉} ([.) \circ i (j)) (k)$
32	12	cv	$setvar z$
33		csumge0	$class sum^$
34		cvol	$class vol$
35	28 34	cfv	$class vol (([.) \circ i (j)) (k))$
36	6 35 21	cprod	$class \prod_{k \in x} vol (([.) \circ i (j)) (k))$
37	20 17 36	cmpt	$class (j \in ℕ ⟼ \prod_{k \in x} vol (([.) \circ i (j)) (k)))$
38	37 33	cfv	$class sum^((j \in ℕ ⟼ \prod_{k \in x} vol (([.) \circ i (j)) (k))))$
39	32 38	wceq	$wff z = sum^((j \in ℕ ⟼ \prod_{k \in x} vol (([.) \circ i (j)) (k))))$
40	31 39	wa	$wff (y \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)))))$
41	40 14 18	wrex	$wff \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))$
42	41 12 13	crab	$class \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\}$
43		clt	$class <$
44	42 13 43	cinf	$class inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\} ℝ^{} <)$
45	10 11 44	cif	$class if (x = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\} ℝ^{} <))$
46	3 8 45	cmpt	$class (y \in 𝒫 (ℝ^{x}) ⟼ if (x = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\} ℝ^{} <)))$
47	1 2 46	cmpt	$class (x \in Fin ⟼ (y \in 𝒫 (ℝ^{x}) ⟼ if (x = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\} ℝ^{} <))))$
48	0 47	wceq	$wff voln* = (x \in Fin ⟼ (y \in 𝒫 (ℝ^{x}) ⟼ if (x = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{x})}^{ℕ}) (y \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)))))\} ℝ^{} <))))$

Metamath Proof Explorer

Definition df-ovoln

Detailed syntax breakdown