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

Definition df-ibl 19517
 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 19511 . 2
2 vx . . . . . . 7
3 cr 8991 . . . . . . 7
4 vy . . . . . . . 8
52cv 1652 . . . . . . . . . . 11
6 vf . . . . . . . . . . . 12
76cv 1652 . . . . . . . . . . 11
85, 7cfv 5456 . . . . . . . . . 10
9 ci 8994 . . . . . . . . . . 11
10 vk . . . . . . . . . . . 12
1110cv 1652 . . . . . . . . . . 11
12 cexp 11384 . . . . . . . . . . 11
139, 11, 12co 6083 . . . . . . . . . 10
14 cdiv 9679 . . . . . . . . . 10
158, 13, 14co 6083 . . . . . . . . 9
16 cre 11904 . . . . . . . . 9
1715, 16cfv 5456 . . . . . . . 8
187cdm 4880 . . . . . . . . . . 11
195, 18wcel 1726 . . . . . . . . . 10
20 cc0 8992 . . . . . . . . . . 11
214cv 1652 . . . . . . . . . . 11
22 cle 9123 . . . . . . . . . . 11
2320, 21, 22wbr 4214 . . . . . . . . . 10
2419, 23wa 360 . . . . . . . . 9
2524, 21, 20cif 3741 . . . . . . . 8
264, 17, 25csb 3253 . . . . . . 7
272, 3, 26cmpt 4268 . . . . . 6
28 citg2 19510 . . . . . 6
2927, 28cfv 5456 . . . . 5
3029, 3wcel 1726 . . . 4
31 c3 10052 . . . . 5
32 cfz 11045 . . . . 5
3320, 31, 32co 6083 . . . 4
3430, 10, 33wral 2707 . . 3
35 cmbf 19508 . . 3 MblFn
3634, 6, 35crab 2711 . 2 MblFn
371, 36wceq 1653 1 MblFn
 Colors of variables: wff set class This definition is referenced by:  isibl  19659  iblmbf  19661
 Copyright terms: Public domain W3C validator