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

Definition df-ovol 18824
 Description: Define the outer Lebesgue measure for subsets of the reals. Here is a function from the natural numbers 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 18822 . 2
2 vx . . 3
3 cr 8736 . . . 4
43cpw 3625 . . 3
52cv 1622 . . . . . . . 8
6 cioo 10656 . . . . . . . . . . 11
7 vf . . . . . . . . . . . 12
87cv 1622 . . . . . . . . . . 11
96, 8ccom 4693 . . . . . . . . . 10
109crn 4690 . . . . . . . . 9
1110cuni 3827 . . . . . . . 8
125, 11wss 3152 . . . . . . 7
13 vy . . . . . . . . 9
1413cv 1622 . . . . . . . 8
15 caddc 8740 . . . . . . . . . . 11
16 cabs 11719 . . . . . . . . . . . . 13
17 cmin 9037 . . . . . . . . . . . . 13
1816, 17ccom 4693 . . . . . . . . . . . 12
1918, 8ccom 4693 . . . . . . . . . . 11
20 c1 8738 . . . . . . . . . . 11
2115, 19, 20cseq 11046 . . . . . . . . . 10
2221crn 4690 . . . . . . . . 9
23 cxr 8866 . . . . . . . . 9
24 clt 8867 . . . . . . . . 9
2522, 23, 24csup 7193 . . . . . . . 8
2614, 25wceq 1623 . . . . . . 7
2712, 26wa 358 . . . . . 6
28 cle 8868 . . . . . . . 8
293, 3cxp 4687 . . . . . . . 8
3028, 29cin 3151 . . . . . . 7
31 cn 9746 . . . . . . 7
32 cmap 6772 . . . . . . 7
3330, 31, 32co 5858 . . . . . 6
3427, 7, 33wrex 2544 . . . . 5
3534, 13, 23crab 2547 . . . 4
3624ccnv 4688 . . . 4
3735, 23, 36csup 7193 . . 3
382, 4, 37cmpt 4077 . 2
391, 38wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  ovolval  18833  ovolf  18841
 Copyright terms: Public domain W3C validator