Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-oms Structured version   Unicode version

Definition df-oms 28419
Description: Define a function constructing an outer measure. See omsval 28420 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.)
Assertion
Ref Expression
df-oms  |- toOMeas  =  ( r  e.  _V  |->  ( a  e.  ~P U. dom  r  |->  sup ( ran  ( x  e.  {
z  e.  ~P dom  r  |  ( a  C_ 
U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) ) )
Distinct variable group:    r, a, x, y, z

Detailed syntax breakdown of Definition df-oms
StepHypRef Expression
1 coms 28418 . 2  class toOMeas
2 vr . . 3  setvar  r
3 cvv 3034 . . 3  class  _V
4 va . . . 4  setvar  a
52cv 1398 . . . . . . 7  class  r
65cdm 4913 . . . . . 6  class  dom  r
76cuni 4163 . . . . 5  class  U. dom  r
87cpw 3927 . . . 4  class  ~P U. dom  r
9 vx . . . . . . 7  setvar  x
104cv 1398 . . . . . . . . . 10  class  a
11 vz . . . . . . . . . . . 12  setvar  z
1211cv 1398 . . . . . . . . . . 11  class  z
1312cuni 4163 . . . . . . . . . 10  class  U. z
1410, 13wss 3389 . . . . . . . . 9  wff  a  C_  U. z
15 com 6599 . . . . . . . . . 10  class  om
16 cdom 7433 . . . . . . . . . 10  class  ~<_
1712, 15, 16wbr 4367 . . . . . . . . 9  wff  z  ~<_  om
1814, 17wa 367 . . . . . . . 8  wff  ( a 
C_  U. z  /\  z  ~<_  om )
196cpw 3927 . . . . . . . 8  class  ~P dom  r
2018, 11, 19crab 2736 . . . . . . 7  class  { z  e.  ~P dom  r  |  ( a  C_  U. z  /\  z  ~<_  om ) }
219cv 1398 . . . . . . . 8  class  x
22 vy . . . . . . . . . 10  setvar  y
2322cv 1398 . . . . . . . . 9  class  y
2423, 5cfv 5496 . . . . . . . 8  class  ( r `
 y )
2521, 24, 22cesum 28175 . . . . . . 7  class Σ* y  e.  x
( r `  y
)
269, 20, 25cmpt 4425 . . . . . 6  class  ( x  e.  { z  e. 
~P dom  r  | 
( a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x ( r `  y ) )
2726crn 4914 . . . . 5  class  ran  (
x  e.  { z  e.  ~P dom  r  |  ( a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) )
28 cc0 9403 . . . . . 6  class  0
29 cpnf 9536 . . . . . 6  class +oo
30 cicc 11453 . . . . . 6  class  [,]
3128, 29, 30co 6196 . . . . 5  class  ( 0 [,] +oo )
32 clt 9539 . . . . . 6  class  <
3332ccnv 4912 . . . . 5  class  `'  <
3427, 31, 33csup 7815 . . . 4  class  sup ( ran  ( x  e.  {
z  e.  ~P dom  r  |  ( a  C_ 
U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) ) ,  ( 0 [,] +oo ) ,  `'  <  )
354, 8, 34cmpt 4425 . . 3  class  ( a  e.  ~P U. dom  r  |->  sup ( ran  (
x  e.  { z  e.  ~P dom  r  |  ( a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
362, 3, 35cmpt 4425 . 2  class  ( r  e.  _V  |->  ( a  e.  ~P U. dom  r  |->  sup ( ran  (
x  e.  { z  e.  ~P dom  r  |  ( a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) ) )
371, 36wceq 1399 1  wff toOMeas  =  ( r  e.  _V  |->  ( a  e.  ~P U. dom  r  |->  sup ( ran  ( x  e.  {
z  e.  ~P dom  r  |  ( a  C_ 
U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  omsval  28420
  Copyright terms: Public domain W3C validator