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

Definition df-ovol 19314
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 19312 . 2  class  vol *
2 vx . . 3  set  x
3 cr 8945 . . . 4  class  RR
43cpw 3759 . . 3  class  ~P RR
52cv 1648 . . . . . . . 8  class  x
6 cioo 10872 . . . . . . . . . . 11  class  (,)
7 vf . . . . . . . . . . . 12  set  f
87cv 1648 . . . . . . . . . . 11  class  f
96, 8ccom 4841 . . . . . . . . . 10  class  ( (,) 
o.  f )
109crn 4838 . . . . . . . . 9  class  ran  ( (,)  o.  f )
1110cuni 3975 . . . . . . . 8  class  U. ran  ( (,)  o.  f )
125, 11wss 3280 . . . . . . 7  wff  x  C_  U.
ran  ( (,)  o.  f )
13 vy . . . . . . . . 9  set  y
1413cv 1648 . . . . . . . 8  class  y
15 caddc 8949 . . . . . . . . . . 11  class  +
16 cabs 11994 . . . . . . . . . . . . 13  class  abs
17 cmin 9247 . . . . . . . . . . . . 13  class  -
1816, 17ccom 4841 . . . . . . . . . . . 12  class  ( abs 
o.  -  )
1918, 8ccom 4841 . . . . . . . . . . 11  class  ( ( abs  o.  -  )  o.  f )
20 c1 8947 . . . . . . . . . . 11  class  1
2115, 19, 20cseq 11278 . . . . . . . . . 10  class  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
2221crn 4838 . . . . . . . . 9  class  ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) )
23 cxr 9075 . . . . . . . . 9  class  RR*
24 clt 9076 . . . . . . . . 9  class  <
2522, 23, 24csup 7403 . . . . . . . 8  class  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )
2614, 25wceq 1649 . . . . . . 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 9077 . . . . . . . 8  class  <_
293, 3cxp 4835 . . . . . . . 8  class  ( RR 
X.  RR )
3028, 29cin 3279 . . . . . . 7  class  (  <_  i^i  ( RR  X.  RR ) )
31 cn 9956 . . . . . . 7  class  NN
32 cmap 6977 . . . . . . 7  class  ^m
3330, 31, 32co 6040 . . . . . 6  class  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )
3427, 7, 33wrex 2667 . . . . 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 2670 . . . 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 4836 . . . 4  class  `'  <
3735, 23, 36csup 7403 . . 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 4226 . 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 1649 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  19323  ovolf  19331
  Copyright terms: Public domain W3C validator