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

Definition df-mbf 21074
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 20984) 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 21069 . 2  class MblFn
2 cre 12578 . . . . . . . . 9  class  Re
3 vf . . . . . . . . . 10  setvar  f
43cv 1368 . . . . . . . . 9  class  f
52, 4ccom 4839 . . . . . . . 8  class  ( Re  o.  f )
65ccnv 4834 . . . . . . 7  class  `' ( Re  o.  f )
7 vx . . . . . . . 8  setvar  x
87cv 1368 . . . . . . 7  class  x
96, 8cima 4838 . . . . . 6  class  ( `' ( Re  o.  f
) " x )
10 cvol 20922 . . . . . . 7  class  vol
1110cdm 4835 . . . . . 6  class  dom  vol
129, 11wcel 1756 . . . . 5  wff  ( `' ( Re  o.  f
) " x )  e.  dom  vol
13 cim 12579 . . . . . . . . 9  class  Im
1413, 4ccom 4839 . . . . . . . 8  class  ( Im  o.  f )
1514ccnv 4834 . . . . . . 7  class  `' ( Im  o.  f )
1615, 8cima 4838 . . . . . 6  class  ( `' ( Im  o.  f
) " x )
1716, 11wcel 1756 . . . . 5  wff  ( `' ( Im  o.  f
) " x )  e.  dom  vol
1812, 17wa 369 . . . 4  wff  ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
19 cioo 11292 . . . . 5  class  (,)
2019crn 4836 . . . 4  class  ran  (,)
2118, 7, 20wral 2710 . . 3  wff  A. x  e.  ran  (,) ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
22 cc 9272 . . . 4  class  CC
23 cr 9273 . . . 4  class  RR
24 cpm 7207 . . . 4  class  ^pm
2522, 23, 24co 6086 . . 3  class  ( CC 
^pm  RR )
2621, 3, 25crab 2714 . 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 1369 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 setvar class
This definition is referenced by:  ismbf1  21079
  Copyright terms: Public domain W3C validator