Definition df-ovol 23233

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.)

Assertion

Ref	Expression
df-ovol	|- vol* = ( x e. ~P RR |-> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )

Distinct variable group:   x, y, f

Detailed syntax breakdown of Definition df-ovol

Step	Hyp	Ref	Expression
1		covol 23231	. 2 class vol*
2		vx	. . 3 setvar x
3		cr 9935	. . . 4 class RR
4	3	cpw 4158	. . 3 class ~P RR
5	2	cv 1482	. . . . . . . 8 class x
6		cioo 12175	. . . . . . . . . . 11 class (,)
7		vf	. . . . . . . . . . . 12 setvar f
8	7	cv 1482	. . . . . . . . . . 11 class f
9	6, 8	ccom 5118	. . . . . . . . . 10 class ( (,) o. f )
10	9	crn 5115	. . . . . . . . 9 class ran ( (,) o. f )
11	10	cuni 4436	. . . . . . . 8 class U. ran ( (,) o. f )
12	5, 11	wss 3574	. . . . . . 7 wff x C_ U. ran ( (,) o. f )
13		vy	. . . . . . . . 9 setvar y
14	13	cv 1482	. . . . . . . 8 class y
15		caddc 9939	. . . . . . . . . . 11 class +
16		cabs 13974	. . . . . . . . . . . . 13 class abs
17		cmin 10266	. . . . . . . . . . . . 13 class -
18	16, 17	ccom 5118	. . . . . . . . . . . 12 class ( abs o. - )
19	18, 8	ccom 5118	. . . . . . . . . . 11 class ( ( abs o. - ) o. f )
20		c1 9937	. . . . . . . . . . 11 class 1
21	15, 19, 20	cseq 12801	. . . . . . . . . 10 class seq 1 ( + , ( ( abs o. - ) o. f ) )
22	21	crn 5115	. . . . . . . . 9 class ran seq 1 ( + , ( ( abs o. - ) o. f ) )
23		cxr 10073	. . . . . . . . 9 class RR*
24		clt 10074	. . . . . . . . 9 class <
25	22, 23, 24	csup 8346	. . . . . . . 8 class sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < )
26	14, 25	wceq 1483	. . . . . . 7 wff y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < )
27	12, 26	wa 384	. . . . . 6 wff ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
28		cle 10075	. . . . . . . 8 class <_
29	3, 3	cxp 5112	. . . . . . . 8 class ( RR X. RR )
30	28, 29	cin 3573	. . . . . . 7 class ( <_ i^i ( RR X. RR ) )
31		cn 11020	. . . . . . 7 class NN
32		cmap 7857	. . . . . . 7 class ^m
33	30, 31, 32	co 6650	. . . . . 6 class ( ( <_ i^i ( RR X. RR ) ) ^m NN )
34	27, 7, 33	wrex 2913	. . . . 5 wff E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
35	34, 13, 23	crab 2916	. . . 4 class { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
36	35, 23, 24	cinf 8347	. . 3 class inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < )
37	2, 4, 36	cmpt 4729	. 2 class ( x e. ~P RR |-> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
38	1, 37	wceq 1483	1 wff vol* = ( x e. ~P RR |-> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )

This definition is referenced by:  ovolval  23242  ovolf  23250