df-ovol

Description: Define the outer Lebesgue measure for subsets of the reals. Here f is a function from the positive integers to pairs <. a , b >. with a <_ b , and the outer volume of the set x is the infimum over all such functions such that the union of the open intervals ( a , b ) covers x of the sum of b - a . (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 17-Sep-2020)

		Ref	Expression
	Assertion	df-ovol	$⊢ {vol}^{} = (x \in 𝒫 ℝ ⟼ sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		covol	$class {vol}^{*}$
1		vx	$setvar x$
2		cr	$class ℝ$
3	2	cpw	$class 𝒫 ℝ$
4		vy	$setvar y$
5		cxr	$class ℝ^{*}$
6		vf	$setvar f$
7		cle	$class \leq$
8	2 2	cxp	$class ℝ^{2}$
9	7 8	cin	$class (\leq \cap ℝ^{2})$
10		cmap	$class ↑_{𝑚}$
11		cn	$class ℕ$
12	9 11 10	co	$class ({(\leq \cap ℝ^{2})}^{ℕ})$
13	1	cv	$setvar x$
14		cioo	$class (.)$
15	6	cv	$setvar f$
16	14 15	ccom	$class ((.) \circ f)$
17	16	crn	$class ran ((.) \circ f)$
18	17	cuni	$class ⋃ ran ((.) \circ f)$
19	13 18	wss	$wff x \subseteq ⋃ ran ((.) \circ f)$
20	4	cv	$setvar y$
21		c1	$class 1$
22		caddc	$class +$
23		cabs	$class abs$
24		cmin	$class -$
25	23 24	ccom	$class (abs \circ -)$
26	25 15	ccom	$class ((abs \circ -) \circ f)$
27	22 26 21	cseq	$class seq 1 (+ ((abs \circ -) \circ f))$
28	27	crn	$class ran seq 1 (+ ((abs \circ -) \circ f))$
29		clt	$class <$
30	28 5 29	csup	$class sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
31	20 30	wceq	$wff y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
32	19 31	wa	$wff (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
33	32 6 12	wrex	$wff \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
34	33 4 5	crab	$class \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
35	34 5 29	cinf	$class sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{*} <)$
36	1 3 35	cmpt	$class (x \in 𝒫 ℝ ⟼ sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{*} <))$
37	0 36	wceq	$wff {vol}^{} = (x \in 𝒫 ℝ ⟼ sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <))$

Metamath Proof Explorer

Definition df-ovol

Detailed syntax breakdown