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

Definition df-itg2 18977
 Description: Define the Lebesgue integral for nonnegative functions. A nonnegative function's integral is the supremum of the integrals of all simple functions that are less than the input function. Note that this may be for functions that take the value on a set of positive measure or functions that are bounded below by a positive number on a set of infinite measure. (Contributed by Mario Carneiro, 28-Jun-2014.)
Assertion
Ref Expression
df-itg2
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-itg2
StepHypRef Expression
1 citg2 18971 . 2
2 vf . . 3
3 cc0 8737 . . . . 5
4 cpnf 8864 . . . . 5
5 cicc 10659 . . . . 5
63, 4, 5co 5858 . . . 4
7 cr 8736 . . . 4
8 cmap 6772 . . . 4
96, 7, 8co 5858 . . 3
10 vg . . . . . . . . 9
1110cv 1622 . . . . . . . 8
122cv 1622 . . . . . . . 8
13 cle 8868 . . . . . . . . 9
1413cofr 6077 . . . . . . . 8
1511, 12, 14wbr 4023 . . . . . . 7
16 vx . . . . . . . . 9
1716cv 1622 . . . . . . . 8
18 citg1 18970 . . . . . . . . 9
1911, 18cfv 5255 . . . . . . . 8
2017, 19wceq 1623 . . . . . . 7
2115, 20wa 358 . . . . . 6
2218cdm 4689 . . . . . 6
2321, 10, 22wrex 2544 . . . . 5
2423, 16cab 2269 . . . 4
25 cxr 8866 . . . 4
26 clt 8867 . . . 4
2724, 25, 26csup 7193 . . 3
282, 9, 27cmpt 4077 . 2
291, 28wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  itg2val  19083
 Copyright terms: Public domain W3C validator