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 27999
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 27998 . 2  class measures
2 vs . . 3  setvar  s
3 csiga 27939 . . . . 5  class sigAlgebra
43crn 5006 . . . 4  class  ran sigAlgebra
54cuni 4251 . . 3  class  U. ran sigAlgebra
62cv 1378 . . . . . 6  class  s
7 cc0 9504 . . . . . . 7  class  0
8 cpnf 9637 . . . . . . 7  class +oo
9 cicc 11544 . . . . . . 7  class  [,]
107, 8, 9co 6295 . . . . . 6  class  ( 0 [,] +oo )
11 vm . . . . . . 7  setvar  m
1211cv 1378 . . . . . 6  class  m
136, 10, 12wf 5590 . . . . 5  wff  m : s --> ( 0 [,] +oo )
14 c0 3790 . . . . . . 7  class  (/)
1514, 12cfv 5594 . . . . . 6  class  ( m `
 (/) )
1615, 7wceq 1379 . . . . 5  wff  ( m `
 (/) )  =  0
17 vx . . . . . . . . . 10  setvar  x
1817cv 1378 . . . . . . . . 9  class  x
19 com 6695 . . . . . . . . 9  class  om
20 cdom 7526 . . . . . . . . 9  class  ~<_
2118, 19, 20wbr 4453 . . . . . . . 8  wff  x  ~<_  om
22 vy . . . . . . . . 9  setvar  y
2322cv 1378 . . . . . . . . 9  class  y
2422, 18, 23wdisj 4423 . . . . . . . 8  wff Disj  y  e.  x  y
2521, 24wa 369 . . . . . . 7  wff  ( x  ~<_  om  /\ Disj  y  e.  x  y )
2618cuni 4251 . . . . . . . . 9  class  U. x
2726, 12cfv 5594 . . . . . . . 8  class  ( m `
 U. x )
2823, 12cfv 5594 . . . . . . . . 9  class  ( m `
 y )
2918, 28, 22cesum 27872 . . . . . . . 8  class Σ* y  e.  x
( m `  y
)
3027, 29wceq 1379 . . . . . . 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 4016 . . . . . 6  class  ~P s
3331, 17, 32wral 2817 . . . . 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 973 . . . 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 2452 . . 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 4511 . 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 1379 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  28000  measval  28001  ismeas  28002  isrnmeas  28003  measbasedom  28005
  Copyright terms: Public domain W3C validator