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

Definition df-meas 26622
Description: Define a measure as a nonnegative countably additive function over a sigma-algebra onto  ( 0 [,] +oo ) (Contributed by Thierry Arnoux, 10-Sep-2016.)
Assertion
Ref Expression
df-meas  |- measures  =  ( s  e.  U. ran sigAlgebra  |->  { m  |  ( m : s --> ( 0 [,] +oo )  /\  ( m `  (/) )  =  0  /\  A. x  e.  ~P  s ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) ) ) } )
Distinct variable group:    x, m, y, s

Detailed syntax breakdown of Definition df-meas
StepHypRef Expression
1 cmeas 26621 . 2  class measures
2 vs . . 3  setvar  s
3 csiga 26562 . . . . 5  class sigAlgebra
43crn 4853 . . . 4  class  ran sigAlgebra
54cuni 4103 . . 3  class  U. ran sigAlgebra
62cv 1368 . . . . . 6  class  s
7 cc0 9294 . . . . . . 7  class  0
8 cpnf 9427 . . . . . . 7  class +oo
9 cicc 11315 . . . . . . 7  class  [,]
107, 8, 9co 6103 . . . . . 6  class  ( 0 [,] +oo )
11 vm . . . . . . 7  setvar  m
1211cv 1368 . . . . . 6  class  m
136, 10, 12wf 5426 . . . . 5  wff  m : s --> ( 0 [,] +oo )
14 c0 3649 . . . . . . 7  class  (/)
1514, 12cfv 5430 . . . . . 6  class  ( m `
 (/) )
1615, 7wceq 1369 . . . . 5  wff  ( m `
 (/) )  =  0
17 vx . . . . . . . . . 10  setvar  x
1817cv 1368 . . . . . . . . 9  class  x
19 com 6488 . . . . . . . . 9  class  om
20 cdom 7320 . . . . . . . . 9  class  ~<_
2118, 19, 20wbr 4304 . . . . . . . 8  wff  x  ~<_  om
22 vy . . . . . . . . 9  setvar  y
2322cv 1368 . . . . . . . . 9  class  y
2422, 18, 23wdisj 4274 . . . . . . . 8  wff Disj  y  e.  x  y
2521, 24wa 369 . . . . . . 7  wff  ( x  ~<_  om  /\ Disj  y  e.  x  y )
2618cuni 4103 . . . . . . . . 9  class  U. x
2726, 12cfv 5430 . . . . . . . 8  class  ( m `
 U. x )
2823, 12cfv 5430 . . . . . . . . 9  class  ( m `
 y )
2918, 28, 22cesum 26495 . . . . . . . 8  class Σ* y  e.  x
( m `  y
)
3027, 29wceq 1369 . . . . . . 7  wff  ( m `
 U. x )  = Σ* y  e.  x ( m `  y )
3125, 30wi 4 . . . . . 6  wff  ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) )
326cpw 3872 . . . . . 6  class  ~P s
3331, 17, 32wral 2727 . . . . 5  wff  A. x  e.  ~P  s ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) )
3413, 16, 33w3a 965 . . . 4  wff  ( m : s --> ( 0 [,] +oo )  /\  ( m `  (/) )  =  0  /\  A. x  e.  ~P  s ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) ) )
3534, 11cab 2429 . . 3  class  { m  |  ( m : s --> ( 0 [,] +oo )  /\  (
m `  (/) )  =  0  /\  A. x  e.  ~P  s ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) ) ) }
362, 5, 35cmpt 4362 . 2  class  ( s  e.  U. ran sigAlgebra  |->  { m  |  ( m : s --> ( 0 [,] +oo )  /\  (
m `  (/) )  =  0  /\  A. x  e.  ~P  s ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) ) ) } )
371, 36wceq 1369 1  wff measures  =  ( s  e.  U. ran sigAlgebra  |->  { m  |  ( m : s --> ( 0 [,] +oo )  /\  ( m `  (/) )  =  0  /\  A. x  e.  ~P  s ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  -> 
( m `  U. x )  = Σ* y  e.  x ( m `  y ) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  measbase  26623  measval  26624  ismeas  26625  isrnmeas  26626  measbasedom  26628
  Copyright terms: Public domain W3C validator