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

Definition df-ovol 19349
Description: Define the outer Lebesgue measure for subsets of the reals. Here  f is a function from the natural numbers 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.)
Assertion
Ref Expression
df-ovol  |-  vol *  =  ( x  e. 
~P RR  |->  sup ( { 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
StepHypRef Expression
1 covol 19347 . 2  class  vol *
2 vx . . 3  set  x
3 cr 8978 . . . 4  class  RR
43cpw 3791 . . 3  class  ~P RR
52cv 1651 . . . . . . . 8  class  x
6 cioo 10905 . . . . . . . . . . 11  class  (,)
7 vf . . . . . . . . . . . 12  set  f
87cv 1651 . . . . . . . . . . 11  class  f
96, 8ccom 4873 . . . . . . . . . 10  class  ( (,) 
o.  f )
109crn 4870 . . . . . . . . 9  class  ran  ( (,)  o.  f )
1110cuni 4007 . . . . . . . 8  class  U. ran  ( (,)  o.  f )
125, 11wss 3312 . . . . . . 7  wff  x  C_  U.
ran  ( (,)  o.  f )
13 vy . . . . . . . . 9  set  y
1413cv 1651 . . . . . . . 8  class  y
15 caddc 8982 . . . . . . . . . . 11  class  +
16 cabs 12027 . . . . . . . . . . . . 13  class  abs
17 cmin 9280 . . . . . . . . . . . . 13  class  -
1816, 17ccom 4873 . . . . . . . . . . . 12  class  ( abs 
o.  -  )
1918, 8ccom 4873 . . . . . . . . . . 11  class  ( ( abs  o.  -  )  o.  f )
20 c1 8980 . . . . . . . . . . 11  class  1
2115, 19, 20cseq 11311 . . . . . . . . . 10  class  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
2221crn 4870 . . . . . . . . 9  class  ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) )
23 cxr 9108 . . . . . . . . 9  class  RR*
24 clt 9109 . . . . . . . . 9  class  <
2522, 23, 24csup 7436 . . . . . . . 8  class  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )
2614, 25wceq 1652 . . . . . . 7  wff  y  =  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )
2712, 26wa 359 . . . . . 6  wff  ( x 
C_  U. ran  ( (,) 
o.  f )  /\  y  =  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
28 cle 9110 . . . . . . . 8  class  <_
293, 3cxp 4867 . . . . . . . 8  class  ( RR 
X.  RR )
3028, 29cin 3311 . . . . . . 7  class  (  <_  i^i  ( RR  X.  RR ) )
31 cn 9989 . . . . . . 7  class  NN
32 cmap 7009 . . . . . . 7  class  ^m
3330, 31, 32co 6072 . . . . . 6  class  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )
3427, 7, 33wrex 2698 . . . . 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* ,  <  ) )
3534, 13, 23crab 2701 . . . 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* ,  <  ) ) }
3624ccnv 4868 . . . 4  class  `'  <
3735, 23, 36csup 7436 . . 3  class  sup ( { 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* ,  `'  <  )
382, 4, 37cmpt 4258 . 2  class  ( x  e.  ~P RR  |->  sup ( { 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* ,  `'  <  ) )
391, 38wceq 1652 1  wff  vol *  =  ( x  e. 
~P RR  |->  sup ( { 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* ,  `'  <  ) )
Colors of variables: wff set class
This definition is referenced by:  ovolval  19358  ovolf  19366
  Copyright terms: Public domain W3C validator