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

Definition df-itg1 18971
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 18965 . 2  class  S.1
2 vf . . 3  set  f
3 cr 8732 . . . . . 6  class  RR
4 vg . . . . . . 7  set  g
54cv 1623 . . . . . 6  class  g
63, 3, 5wf 5218 . . . . 5  wff  g : RR --> RR
75crn 4690 . . . . . 6  class  ran  g
8 cfn 6859 . . . . . 6  class  Fin
97, 8wcel 1685 . . . . 5  wff  ran  g  e.  Fin
105ccnv 4688 . . . . . . . 8  class  `' g
11 cc0 8733 . . . . . . . . . 10  class  0
1211csn 3642 . . . . . . . . 9  class  { 0 }
133, 12cdif 3151 . . . . . . . 8  class  ( RR 
\  { 0 } )
1410, 13cima 4692 . . . . . . 7  class  ( `' g " ( RR 
\  { 0 } ) )
15 cvol 18818 . . . . . . 7  class  vol
1614, 15cfv 5222 . . . . . 6  class  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )
1716, 3wcel 1685 . . . . 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 18964 . . . 4  class MblFn
2018, 4, 19crab 2549 . . 3  class  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }
212cv 1623 . . . . . 6  class  f
2221crn 4690 . . . . 5  class  ran  f
2322, 12cdif 3151 . . . 4  class  ( ran  f  \  { 0 } )
24 vx . . . . . 6  set  x
2524cv 1623 . . . . 5  class  x
2621ccnv 4688 . . . . . . 7  class  `' f
2725csn 3642 . . . . . . 7  class  { x }
2826, 27cima 4692 . . . . . 6  class  ( `' f " { x } )
2928, 15cfv 5222 . . . . 5  class  ( vol `  ( `' f " { x } ) )
30 cmul 8738 . . . . 5  class  x.
3125, 29, 30co 5820 . . . 4  class  ( x  x.  ( vol `  ( `' f " {
x } ) ) )
3223, 31, 24csu 12153 . . 3  class  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) )
332, 20, 32cmpt 4079 . 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 1624 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  19024  itg1val  19033
  Copyright terms: Public domain W3C validator