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

Definition df-mbf 19500
 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 19410) 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-mbf
StepHypRef Expression
1 cmbf 19494 . 2 MblFn
2 cre 11890 . . . . . . . . 9
3 vf . . . . . . . . . 10
43cv 1651 . . . . . . . . 9
52, 4ccom 4873 . . . . . . . 8
65ccnv 4868 . . . . . . 7
7 vx . . . . . . . 8
87cv 1651 . . . . . . 7
96, 8cima 4872 . . . . . 6
10 cvol 19348 . . . . . . 7
1110cdm 4869 . . . . . 6
129, 11wcel 1725 . . . . 5
13 cim 11891 . . . . . . . . 9
1413, 4ccom 4873 . . . . . . . 8
1514ccnv 4868 . . . . . . 7
1615, 8cima 4872 . . . . . 6
1716, 11wcel 1725 . . . . 5
1812, 17wa 359 . . . 4
19 cioo 10905 . . . . 5
2019crn 4870 . . . 4
2118, 7, 20wral 2697 . . 3
22 cc 8977 . . . 4
23 cr 8978 . . . 4
24 cpm 7010 . . . 4
2522, 23, 24co 6072 . . 3
2621, 3, 25crab 2701 . 2
271, 26wceq 1652 1 MblFn
 Colors of variables: wff set class This definition is referenced by:  ismbf1  19506
 Copyright terms: Public domain W3C validator