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

Definition df-mbf 22113
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 22022) 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 22108 . 2  class MblFn
2 cre 12932 . . . . . . . . 9  class  Re
3 vf . . . . . . . . . 10  setvar  f
43cv 1398 . . . . . . . . 9  class  f
52, 4ccom 4917 . . . . . . . 8  class  ( Re  o.  f )
65ccnv 4912 . . . . . . 7  class  `' ( Re  o.  f )
7 vx . . . . . . . 8  setvar  x
87cv 1398 . . . . . . 7  class  x
96, 8cima 4916 . . . . . 6  class  ( `' ( Re  o.  f
) " x )
10 cvol 21960 . . . . . . 7  class  vol
1110cdm 4913 . . . . . 6  class  dom  vol
129, 11wcel 1826 . . . . 5  wff  ( `' ( Re  o.  f
) " x )  e.  dom  vol
13 cim 12933 . . . . . . . . 9  class  Im
1413, 4ccom 4917 . . . . . . . 8  class  ( Im  o.  f )
1514ccnv 4912 . . . . . . 7  class  `' ( Im  o.  f )
1615, 8cima 4916 . . . . . 6  class  ( `' ( Im  o.  f
) " x )
1716, 11wcel 1826 . . . . 5  wff  ( `' ( Im  o.  f
) " x )  e.  dom  vol
1812, 17wa 367 . . . 4  wff  ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
19 cioo 11450 . . . . 5  class  (,)
2019crn 4914 . . . 4  class  ran  (,)
2118, 7, 20wral 2732 . . 3  wff  A. x  e.  ran  (,) ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
22 cc 9401 . . . 4  class  CC
23 cr 9402 . . . 4  class  RR
24 cpm 7339 . . . 4  class  ^pm
2522, 23, 24co 6196 . . 3  class  ( CC 
^pm  RR )
2621, 3, 25crab 2736 . 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 1399 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  22118
  Copyright terms: Public domain W3C validator