Metamath Proof Explorer

Definition df-ovol

Description: Define the outer Lebesgue measure for subsets of the reals. Here f is a function from the positive integers 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) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion df-ovol 
|- vol* = ( x e. ~P RR |-> inf ( { 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* , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 covol 
 |-  vol*
1 vx 
 |-  x
2 cr 
 |-  RR
3 2 cpw 
 |-  ~P RR
4 vy 
 |-  y
5 cxr 
 |-  RR*
6 vf 
 |-  f
7 cle 
 |-  <_
8 2 2 cxp 
 |-  ( RR X. RR )
9 7 8 cin 
 |-  ( <_ i^i ( RR X. RR ) )
10 cmap 
 |-  ^m
11 cn 
 |-  NN
12 9 11 10 co 
 |-  ( ( <_ i^i ( RR X. RR ) ) ^m NN )
13 1 cv 
 |-  x
14 cioo 
 |-  (,)
15 6 cv 
 |-  f
16 14 15 ccom 
 |-  ( (,) o. f )
17 16 crn 
 |-  ran ( (,) o. f )
18 17 cuni 
 |-  U. ran ( (,) o. f )
19 13 18 wss 
 |-  x C_ U. ran ( (,) o. f )
20 4 cv 
 |-  y
21 c1 
 |-  1
22 caddc 
 |-  +
23 cabs 
 |-  abs
24 cmin 
 |-  -
25 23 24 ccom 
 |-  ( abs o. - )
26 25 15 ccom 
 |-  ( ( abs o. - ) o. f )
27 22 26 21 cseq 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) )
28 27 crn 
 |-  ran seq 1 ( + , ( ( abs o. - ) o. f ) )
29 clt 
 |-  <
30 28 5 29 csup 
 |-  sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < )
31 20 30 wceq 
 |-  y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < )
32 19 31 wa 
 |-  ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
33 32 6 12 wrex 
 |-  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* , < ) )
34 33 4 5 crab 
 |-  { 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* , < ) ) }
35 34 5 29 cinf 
 |-  inf ( { 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* , < )
36 1 3 35 cmpt 
 |-  ( x e. ~P RR |-> inf ( { 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* , < ) )
37 0 36 wceq 
 |-  vol* = ( x e. ~P RR |-> inf ( { 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* , < ) )