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

Definition df-mbf 19190
Description: Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl 19100) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
Assertion
Ref Expression
df-mbf  |- MblFn  =  {
f  e.  ( CC 
^pm  RR )  |  A. x  e.  ran  (,) (
( `' ( Re  o.  f ) "
x )  e.  dom  vol 
/\  ( `' ( Im  o.  f )
" x )  e. 
dom  vol ) }
Distinct variable group:    x, f

Detailed syntax breakdown of Definition df-mbf
StepHypRef Expression
1 cmbf 19184 . 2  class MblFn
2 cre 11789 . . . . . . . . 9  class  Re
3 vf . . . . . . . . . 10  set  f
43cv 1646 . . . . . . . . 9  class  f
52, 4ccom 4796 . . . . . . . 8  class  ( Re  o.  f )
65ccnv 4791 . . . . . . 7  class  `' ( Re  o.  f )
7 vx . . . . . . . 8  set  x
87cv 1646 . . . . . . 7  class  x
96, 8cima 4795 . . . . . 6  class  ( `' ( Re  o.  f
) " x )
10 cvol 19038 . . . . . . 7  class  vol
1110cdm 4792 . . . . . 6  class  dom  vol
129, 11wcel 1715 . . . . 5  wff  ( `' ( Re  o.  f
) " x )  e.  dom  vol
13 cim 11790 . . . . . . . . 9  class  Im
1413, 4ccom 4796 . . . . . . . 8  class  ( Im  o.  f )
1514ccnv 4791 . . . . . . 7  class  `' ( Im  o.  f )
1615, 8cima 4795 . . . . . 6  class  ( `' ( Im  o.  f
) " x )
1716, 11wcel 1715 . . . . 5  wff  ( `' ( Im  o.  f
) " x )  e.  dom  vol
1812, 17wa 358 . . . 4  wff  ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
19 cioo 10809 . . . . 5  class  (,)
2019crn 4793 . . . 4  class  ran  (,)
2118, 7, 20wral 2628 . . 3  wff  A. x  e.  ran  (,) ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
22 cc 8882 . . . 4  class  CC
23 cr 8883 . . . 4  class  RR
24 cpm 6916 . . . 4  class  ^pm
2522, 23, 24co 5981 . . 3  class  ( CC 
^pm  RR )
2621, 3, 25crab 2632 . 2  class  { f  e.  ( CC  ^pm  RR )  |  A. x  e.  ran  (,) ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol ) }
271, 26wceq 1647 1  wff MblFn  =  {
f  e.  ( CC 
^pm  RR )  |  A. x  e.  ran  (,) (
( `' ( Re  o.  f ) "
x )  e.  dom  vol 
/\  ( `' ( Im  o.  f )
" x )  e. 
dom  vol ) }
Colors of variables: wff set class
This definition is referenced by:  ismbf1  19196
  Copyright terms: Public domain W3C validator