This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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* , < ) )