Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ovol Structured version   Unicode version

Definition df-ovol 22287
 Description: Define the outer Lebesgue measure for subsets of the reals. Here is a function from the positive integers to pairs with , and the outer volume of the set is the infimum over all such functions such that the union of the open intervals covers of the sum of . (Contributed by Mario Carneiro, 16-Mar-2014.)
Assertion
Ref Expression
df-ovol
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ovol
StepHypRef Expression
1 covol 22285 . 2
2 vx . . 3
3 cr 9537 . . . 4
43cpw 3985 . . 3
52cv 1436 . . . . . . . 8
6 cioo 11635 . . . . . . . . . . 11
7 vf . . . . . . . . . . . 12
87cv 1436 . . . . . . . . . . 11
96, 8ccom 4858 . . . . . . . . . 10
109crn 4855 . . . . . . . . 9
1110cuni 4222 . . . . . . . 8
125, 11wss 3442 . . . . . . 7
13 vy . . . . . . . . 9
1413cv 1436 . . . . . . . 8
15 caddc 9541 . . . . . . . . . . 11
16 cabs 13276 . . . . . . . . . . . . 13
17 cmin 9859 . . . . . . . . . . . . 13
1816, 17ccom 4858 . . . . . . . . . . . 12
1918, 8ccom 4858 . . . . . . . . . . 11
20 c1 9539 . . . . . . . . . . 11
2115, 19, 20cseq 12210 . . . . . . . . . 10
2221crn 4855 . . . . . . . . 9
23 cxr 9673 . . . . . . . . 9
24 clt 9674 . . . . . . . . 9
2522, 23, 24csup 7960 . . . . . . . 8
2614, 25wceq 1437 . . . . . . 7
2712, 26wa 370 . . . . . 6
28 cle 9675 . . . . . . . 8
293, 3cxp 4852 . . . . . . . 8
3028, 29cin 3441 . . . . . . 7
31 cn 10609 . . . . . . 7
32 cmap 7480 . . . . . . 7
3330, 31, 32co 6305 . . . . . 6
3427, 7, 33wrex 2783 . . . . 5
3534, 13, 23crab 2786 . . . 4
3624ccnv 4853 . . . 4
3735, 23, 36csup 7960 . . 3
382, 4, 37cmpt 4484 . 2
391, 38wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  ovolval  22296  ovolf  22304
 Copyright terms: Public domain W3C validator