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

Definition df-mbf 18975
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 18885) 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 18969 . 2  class MblFn
2 cre 11582 . . . . . . . . 9  class  Re
3 vf . . . . . . . . . 10  set  f
43cv 1622 . . . . . . . . 9  class  f
52, 4ccom 4693 . . . . . . . 8  class  ( Re  o.  f )
65ccnv 4688 . . . . . . 7  class  `' ( Re  o.  f )
7 vx . . . . . . . 8  set  x
87cv 1622 . . . . . . 7  class  x
96, 8cima 4692 . . . . . 6  class  ( `' ( Re  o.  f
) " x )
10 cvol 18823 . . . . . . 7  class  vol
1110cdm 4689 . . . . . 6  class  dom  vol
129, 11wcel 1684 . . . . 5  wff  ( `' ( Re  o.  f
) " x )  e.  dom  vol
13 cim 11583 . . . . . . . . 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 1684 . . . . 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 10656 . . . . 5  class  (,)
2019crn 4690 . . . 4  class  ran  (,)
2118, 7, 20wral 2543 . . 3  wff  A. x  e.  ran  (,) ( ( `' ( Re  o.  f ) " x
)  e.  dom  vol  /\  ( `' ( Im  o.  f ) "
x )  e.  dom  vol )
22 cc 8735 . . . 4  class  CC
23 cr 8736 . . . 4  class  RR
24 cpm 6773 . . . 4  class  ^pm
2522, 23, 24co 5858 . . 3  class  ( CC 
^pm  RR )
2621, 3, 25crab 2547 . 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 1623 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  18981
  Copyright terms: Public domain W3C validator