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

Definition df-mbf 18970
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 18880) 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 18964 . 2  class MblFn
2 cre 11577 . . . . . . . . 9  class  Re
3 vf . . . . . . . . . 10  set  f
43cv 1623 . . . . . . . . 9  class  f
52, 4ccom 4693 . . . . . . . 8  class  ( Re  o.  f )
65ccnv 4688 . . . . . . 7  class  `' ( Re  o.  f )
7 vx . . . . . . . 8  set  x
87cv 1623 . . . . . . 7  class  x
96, 8cima 4692 . . . . . 6  class  ( `' ( Re  o.  f
) " x )
10 cvol 18818 . . . . . . 7  class  vol
1110cdm 4689 . . . . . 6  class  dom  vol
129, 11wcel 1685 . . . . 5  wff  ( `' ( Re  o.  f
) " x )  e.  dom  vol
13 cim 11578 . . . . . . . . 9  class  Im
1413, 4ccom 4693 . . . . . . . 8  class  ( Im  o.  f )
1514ccnv 4688 . . . . . . 7  class  `' ( Im  o.  f )
1615, 8cima 4692 . . . . . 6  class  ( `' ( Im  o.  f
) " x )
1716, 11wcel 1685 . . . . 5  wff  ( `' ( Im  o.  f
) " x )  e.  dom  vol
1812, 17wa 360 . . . 4  wff  ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
19 cioo 10651 . . . . 5  class  (,)
2019crn 4690 . . . 4  class  ran  (,)
2118, 7, 20wral 2545 . . 3  wff  A. x  e.  ran  (,) ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
22 cc 8731 . . . 4  class  CC
23 cr 8732 . . . 4  class  RR
24 cpm 6769 . . . 4  class  ^pm
2522, 23, 24co 5820 . . 3  class  ( CC 
^pm  RR )
2621, 3, 25crab 2549 . 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 1624 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  18976
  Copyright terms: Public domain W3C validator