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 ∫2 = ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 citg2 ⊢ ∫2
1 vf ⊢ 𝑓
2 cc0 ⊢ 0
3 cicc ⊢ [,]
4 cpnf ⊢ +∞
5 2 4 3 co ⊢ ( 0 [,] +∞ )
6 cmap ⊢ ↑m
7 cr ⊢ ℝ
8 5 7 6 co ⊢ ( ( 0 [,] +∞ ) ↑m ℝ )
9 vx ⊢ 𝑥
10 vg ⊢ 𝑔
11 citg1 ⊢ ∫1
12 11 cdm ⊢ dom ∫1
13 10 cv ⊢ 𝑔
14 cle ⊢ ≤
15 14 cofr ⊢ ∘r ≤
16 1 cv ⊢ 𝑓
17 13 16 15 wbr ⊢ 𝑔 ∘r ≤ 𝑓
18 9 cv ⊢ 𝑥
19 13 11 cfv ⊢ ( ∫1 ‘ 𝑔 )
20 18 19 wceq ⊢ 𝑥 = ( ∫1 ‘ 𝑔 )
21 17 20 wa ⊢ ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) )
22 21 10 12 wrex ⊢ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) )
23 22 9 cab ⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
24 cxr ⊢ ℝ*
25 clt ⊢ <
26 23 24 25 csup ⊢ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < )
27 1 8 26 cmpt ⊢ ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
28 0 27 wceq ⊢ ∫2 = ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )