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 26846
Description: Define a function constructing an outer measure. See omsval 26847 for its value. (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 ~P U.
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 26845 . 2  class toOMeas
2 vr . . 3  setvar  r
3 cvv 3072 . . 3  class  _V
4 va . . . 4  setvar  a
52cv 1369 . . . . . . 7  class  r
65cdm 4943 . . . . . 6  class  dom  r
76cuni 4194 . . . . 5  class  U. dom  r
87cpw 3963 . . . 4  class  ~P U. dom  r
9 vx . . . . . . 7  setvar  x
104cv 1369 . . . . . . . . . 10  class  a
11 vz . . . . . . . . . . . 12  setvar  z
1211cv 1369 . . . . . . . . . . 11  class  z
1312cuni 4194 . . . . . . . . . 10  class  U. z
1410, 13wss 3431 . . . . . . . . 9  wff  a  C_  U. z
15 com 6581 . . . . . . . . . 10  class  om
16 cdom 7413 . . . . . . . . . 10  class  ~<_
1712, 15, 16wbr 4395 . . . . . . . . 9  wff  z  ~<_  om
1814, 17wa 369 . . . . . . . 8  wff  ( a 
C_  U. z  /\  z  ~<_  om )
198cpw 3963 . . . . . . . 8  class  ~P ~P U.
dom  r
2018, 11, 19crab 2800 . . . . . . 7  class  { z  e.  ~P ~P U. dom  r  |  (
a  C_  U. z  /\  z  ~<_  om ) }
219cv 1369 . . . . . . . 8  class  x
22 vy . . . . . . . . . 10  setvar  y
2322cv 1369 . . . . . . . . 9  class  y
2423, 5cfv 5521 . . . . . . . 8  class  ( r `
 y )
2521, 24, 22cesum 26623 . . . . . . 7  class Σ* y  e.  x
( r `  y
)
269, 20, 25cmpt 4453 . . . . . 6  class  ( x  e.  { z  e. 
~P ~P U. dom  r  |  ( a  C_ 
U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x
( r `  y
) )
2726crn 4944 . . . . 5  class  ran  (
x  e.  { z  e.  ~P ~P U. dom  r  |  (
a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x ( r `  y ) )
28 cc0 9388 . . . . . 6  class  0
29 cpnf 9521 . . . . . 6  class +oo
30 cicc 11409 . . . . . 6  class  [,]
3128, 29, 30co 6195 . . . . 5  class  ( 0 [,] +oo )
32 clt 9524 . . . . . 6  class  <
3332ccnv 4942 . . . . 5  class  `'  <
3427, 31, 33csup 7796 . . . 4  class  sup ( ran  ( x  e.  {
z  e.  ~P ~P U.
dom  r  |  ( a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x ( r `  y ) ) ,  ( 0 [,] +oo ) ,  `'  <  )
354, 8, 34cmpt 4453 . . 3  class  ( a  e.  ~P U. dom  r  |->  sup ( ran  (
x  e.  { z  e.  ~P ~P U. dom  r  |  (
a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x ( r `  y ) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
362, 3, 35cmpt 4453 . 2  class  ( r  e.  _V  |->  ( a  e.  ~P U. dom  r  |->  sup ( ran  (
x  e.  { z  e.  ~P ~P U. dom  r  |  (
a  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* y  e.  x ( r `  y ) ) ,  ( 0 [,] +oo ) ,  `'  <  ) ) )
371, 36wceq 1370 1  wff toOMeas  =  ( r  e.  _V  |->  ( a  e.  ~P U. dom  r  |->  sup ( ran  ( x  e.  {
z  e.  ~P ~P U.
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  26847
  Copyright terms: Public domain W3C validator