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

Definition df-ibl 18978
 Description: Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014.)
Assertion
Ref Expression
df-ibl MblFn
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-ibl
StepHypRef Expression
1 cibl 18972 . 2
2 vx . . . . . . 7
3 cr 8736 . . . . . . 7
4 vy . . . . . . . 8
52cv 1622 . . . . . . . . . . 11
6 vf . . . . . . . . . . . 12
76cv 1622 . . . . . . . . . . 11
85, 7cfv 5255 . . . . . . . . . 10
9 ci 8739 . . . . . . . . . . 11
10 vk . . . . . . . . . . . 12
1110cv 1622 . . . . . . . . . . 11
12 cexp 11104 . . . . . . . . . . 11
139, 11, 12co 5858 . . . . . . . . . 10
14 cdiv 9423 . . . . . . . . . 10
158, 13, 14co 5858 . . . . . . . . 9
16 cre 11582 . . . . . . . . 9
1715, 16cfv 5255 . . . . . . . 8
187cdm 4689 . . . . . . . . . . 11
195, 18wcel 1684 . . . . . . . . . 10
20 cc0 8737 . . . . . . . . . . 11
214cv 1622 . . . . . . . . . . 11
22 cle 8868 . . . . . . . . . . 11
2320, 21, 22wbr 4023 . . . . . . . . . 10
2419, 23wa 358 . . . . . . . . 9
2524, 21, 20cif 3565 . . . . . . . 8
264, 17, 25csb 3081 . . . . . . 7
272, 3, 26cmpt 4077 . . . . . 6
28 citg2 18971 . . . . . 6
2927, 28cfv 5255 . . . . 5
3029, 3wcel 1684 . . . 4
31 c3 9796 . . . . 5
32 cfz 10782 . . . . 5
3320, 31, 32co 5858 . . . 4
3430, 10, 33wral 2543 . . 3
35 cmbf 18969 . . 3 MblFn
3634, 6, 35crab 2547 . 2 MblFn
371, 36wceq 1623 1 MblFn
 Colors of variables: wff set class This definition is referenced by:  isibl  19120  iblmbf  19122
 Copyright terms: Public domain W3C validator