Metamath Proof Explorer


Definition df-itg2

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 +oo for functions that take the value +oo 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)

Ref Expression
Assertion df-itg2
|- S.2 = ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 citg2
 |-  S.2
1 vf
 |-  f
2 cc0
 |-  0
3 cicc
 |-  [,]
4 cpnf
 |-  +oo
5 2 4 3 co
 |-  ( 0 [,] +oo )
6 cmap
 |-  ^m
7 cr
 |-  RR
8 5 7 6 co
 |-  ( ( 0 [,] +oo ) ^m RR )
9 vx
 |-  x
10 vg
 |-  g
11 citg1
 |-  S.1
12 11 cdm
 |-  dom S.1
13 10 cv
 |-  g
14 cle
 |-  <_
15 14 cofr
 |-  oR <_
16 1 cv
 |-  f
17 13 16 15 wbr
 |-  g oR <_ f
18 9 cv
 |-  x
19 13 11 cfv
 |-  ( S.1 ` g )
20 18 19 wceq
 |-  x = ( S.1 ` g )
21 17 20 wa
 |-  ( g oR <_ f /\ x = ( S.1 ` g ) )
22 21 10 12 wrex
 |-  E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) )
23 22 9 cab
 |-  { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) }
24 cxr
 |-  RR*
25 clt
 |-  <
26 23 24 25 csup
 |-  sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < )
27 1 8 26 cmpt
 |-  ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )
28 0 27 wceq
 |-  S.2 = ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )