MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-itg1 Unicode version

Definition df-itg1 19466
Description: Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
df-itg1  |-  S.1  =  ( f  e.  {
g  e. MblFn  |  (
g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR ) }  |->  sum_
x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f " {
x } ) ) ) )
Distinct variable group:    f, g, x

Detailed syntax breakdown of Definition df-itg1
StepHypRef Expression
1 citg1 19460 . 2  class  S.1
2 vf . . 3  set  f
3 cr 8945 . . . . . 6  class  RR
4 vg . . . . . . 7  set  g
54cv 1648 . . . . . 6  class  g
63, 3, 5wf 5409 . . . . 5  wff  g : RR --> RR
75crn 4838 . . . . . 6  class  ran  g
8 cfn 7068 . . . . . 6  class  Fin
97, 8wcel 1721 . . . . 5  wff  ran  g  e.  Fin
105ccnv 4836 . . . . . . . 8  class  `' g
11 cc0 8946 . . . . . . . . . 10  class  0
1211csn 3774 . . . . . . . . 9  class  { 0 }
133, 12cdif 3277 . . . . . . . 8  class  ( RR 
\  { 0 } )
1410, 13cima 4840 . . . . . . 7  class  ( `' g " ( RR 
\  { 0 } ) )
15 cvol 19313 . . . . . . 7  class  vol
1614, 15cfv 5413 . . . . . 6  class  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )
1716, 3wcel 1721 . . . . 5  wff  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )  e.  RR
186, 9, 17w3a 936 . . . 4  wff  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR )
19 cmbf 19459 . . . 4  class MblFn
2018, 4, 19crab 2670 . . 3  class  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }
212cv 1648 . . . . . 6  class  f
2221crn 4838 . . . . 5  class  ran  f
2322, 12cdif 3277 . . . 4  class  ( ran  f  \  { 0 } )
24 vx . . . . . 6  set  x
2524cv 1648 . . . . 5  class  x
2621ccnv 4836 . . . . . . 7  class  `' f
2725csn 3774 . . . . . . 7  class  { x }
2826, 27cima 4840 . . . . . 6  class  ( `' f " { x } )
2928, 15cfv 5413 . . . . 5  class  ( vol `  ( `' f " { x } ) )
30 cmul 8951 . . . . 5  class  x.
3125, 29, 30co 6040 . . . 4  class  ( x  x.  ( vol `  ( `' f " {
x } ) ) )
3223, 31, 24csu 12434 . . 3  class  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) )
332, 20, 32cmpt 4226 . 2  class  ( f  e.  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }  |->  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) ) )
341, 33wceq 1649 1  wff  S.1  =  ( f  e.  {
g  e. MblFn  |  (
g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR ) }  |->  sum_
x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f " {
x } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  isi1f  19519  itg1val  19528
  Copyright terms: Public domain W3C validator