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

Definition df-itg1 19517
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 19512 . 2  class  S.1
2 vf . . 3  set  f
3 cr 8994 . . . . . 6  class  RR
4 vg . . . . . . 7  set  g
54cv 1652 . . . . . 6  class  g
63, 3, 5wf 5453 . . . . 5  wff  g : RR --> RR
75crn 4882 . . . . . 6  class  ran  g
8 cfn 7112 . . . . . 6  class  Fin
97, 8wcel 1726 . . . . 5  wff  ran  g  e.  Fin
105ccnv 4880 . . . . . . . 8  class  `' g
11 cc0 8995 . . . . . . . . . 10  class  0
1211csn 3816 . . . . . . . . 9  class  { 0 }
133, 12cdif 3319 . . . . . . . 8  class  ( RR 
\  { 0 } )
1410, 13cima 4884 . . . . . . 7  class  ( `' g " ( RR 
\  { 0 } ) )
15 cvol 19365 . . . . . . 7  class  vol
1614, 15cfv 5457 . . . . . 6  class  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )
1716, 3wcel 1726 . . . . 5  wff  ( vol `  ( `' g "
( RR  \  {
0 } ) ) )  e.  RR
186, 9, 17w3a 937 . . . 4  wff  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g " ( RR  \  { 0 } ) ) )  e.  RR )
19 cmbf 19511 . . . 4  class MblFn
2018, 4, 19crab 2711 . . 3  class  { g  e. MblFn  |  ( g : RR --> RR  /\  ran  g  e.  Fin  /\  ( vol `  ( `' g
" ( RR  \  { 0 } ) ) )  e.  RR ) }
212cv 1652 . . . . . 6  class  f
2221crn 4882 . . . . 5  class  ran  f
2322, 12cdif 3319 . . . 4  class  ( ran  f  \  { 0 } )
24 vx . . . . . 6  set  x
2524cv 1652 . . . . 5  class  x
2621ccnv 4880 . . . . . . 7  class  `' f
2725csn 3816 . . . . . . 7  class  { x }
2826, 27cima 4884 . . . . . 6  class  ( `' f " { x } )
2928, 15cfv 5457 . . . . 5  class  ( vol `  ( `' f " { x } ) )
30 cmul 9000 . . . . 5  class  x.
3125, 29, 30co 6084 . . . 4  class  ( x  x.  ( vol `  ( `' f " {
x } ) ) )
3223, 31, 24csu 12484 . . 3  class  sum_ x  e.  ( ran  f  \  { 0 } ) ( x  x.  ( vol `  ( `' f
" { x }
) ) )
332, 20, 32cmpt 4269 . 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 1653 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  19569  itg1val  19578
  Copyright terms: Public domain W3C validator