MPE Home 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  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 18822 . 2  class  vol *
2 vx . . 3  set  x
3 cr 8736 . . . 4  class  RR
43cpw 3625 . . 3  class  ~P RR
52cv 1622 . . . . . . . 8  class  x
6 cioo 10656 . . . . . . . . . . 11  class  (,)
7 vf . . . . . . . . . . . 12  set  f
87cv 1622 . . . . . . . . . . 11  class  f
96, 8ccom 4693 . . . . . . . . . 10  class  ( (,) 
o.  f )
109crn 4690 . . . . . . . . 9  class  ran  ( (,)  o.  f )
1110cuni 3827 . . . . . . . 8  class  U. ran  ( (,)  o.  f )
125, 11wss 3152 . . . . . . 7  wff  x  C_  U.
ran  ( (,)  o.  f )
13 vy . . . . . . . . 9  set  y
1413cv 1622 . . . . . . . 8  class  y
15 caddc 8740 . . . . . . . . . . 11  class  +
16 cabs 11719 . . . . . . . . . . . . 13  class  abs
17 cmin 9037 . . . . . . . . . . . . 13  class  -
1816, 17ccom 4693 . . . . . . . . . . . 12  class  ( abs 
o.  -  )
1918, 8ccom 4693 . . . . . . . . . . 11  class  ( ( abs  o.  -  )  o.  f )
20 c1 8738 . . . . . . . . . . 11  class  1
2115, 19, 20cseq 11046 . . . . . . . . . 10  class  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
2221crn 4690 . . . . . . . . 9  class  ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) )
23 cxr 8866 . . . . . . . . 9  class  RR*
24 clt 8867 . . . . . . . . 9  class  <
2522, 23, 24csup 7193 . . . . . . . 8  class  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )
2614, 25wceq 1623 . . . . . . 7  wff  y  =  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )
2712, 26wa 358 . . . . . 6  wff  ( x 
C_  U. ran  ( (,) 
o.  f )  /\  y  =  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
28 cle 8868 . . . . . . . 8  class  <_
293, 3cxp 4687 . . . . . . . 8  class  ( RR 
X.  RR )
3028, 29cin 3151 . . . . . . 7  class  (  <_  i^i  ( RR  X.  RR ) )
31 cn 9746 . . . . . . 7  class  NN
32 cmap 6772 . . . . . . 7  class  ^m
3330, 31, 32co 5858 . . . . . 6  class  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )
3427, 7, 33wrex 2544 . . . . 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 2547 . . . 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 4688 . . . 4  class  `'  <
3735, 23, 36csup 7193 . . 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 4077 . 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 1623 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  18833  ovolf  18841
  Copyright terms: Public domain W3C validator