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

Definition df-ovol 22494
 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.) (Revised by AV, 17-Sep-2020.)
Assertion
Ref Expression
df-ovol inf
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ovol
StepHypRef Expression
1 covol 22491 . 2
2 vx . . 3
3 cr 9556 . . . 4
43cpw 3942 . . 3
52cv 1451 . . . . . . . 8
6 cioo 11660 . . . . . . . . . . 11
7 vf . . . . . . . . . . . 12
87cv 1451 . . . . . . . . . . 11
96, 8ccom 4843 . . . . . . . . . 10
109crn 4840 . . . . . . . . 9
1110cuni 4190 . . . . . . . 8
125, 11wss 3390 . . . . . . 7
13 vy . . . . . . . . 9
1413cv 1451 . . . . . . . 8
15 caddc 9560 . . . . . . . . . . 11
16 cabs 13374 . . . . . . . . . . . . 13
17 cmin 9880 . . . . . . . . . . . . 13
1816, 17ccom 4843 . . . . . . . . . . . 12
1918, 8ccom 4843 . . . . . . . . . . 11
20 c1 9558 . . . . . . . . . . 11
2115, 19, 20cseq 12251 . . . . . . . . . 10
2221crn 4840 . . . . . . . . 9
23 cxr 9692 . . . . . . . . 9
24 clt 9693 . . . . . . . . 9
2522, 23, 24csup 7972 . . . . . . . 8
2614, 25wceq 1452 . . . . . . 7
2712, 26wa 376 . . . . . 6
28 cle 9694 . . . . . . . 8
293, 3cxp 4837 . . . . . . . 8
3028, 29cin 3389 . . . . . . 7
31 cn 10631 . . . . . . 7
32 cmap 7490 . . . . . . 7
3330, 31, 32co 6308 . . . . . 6
3427, 7, 33wrex 2757 . . . . 5
3534, 13, 23crab 2760 . . . 4
3635, 23, 24cinf 7973 . . 3 inf
372, 4, 36cmpt 4454 . 2 inf
381, 37wceq 1452 1 inf
 Colors of variables: wff setvar class This definition is referenced by:  ovolval  22504  ovolf  22513
 Copyright terms: Public domain W3C validator