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 = f ∈ 0 +∞ ℝ ⟼ sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f f ∧ x = ∫ 1 ⁡ g ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 citg2 class ∫ 2
1 vf setvar f
2 cc0 class 0
3 cicc class .
4 cpnf class +∞
5 2 4 3 co class 0 +∞
6 cmap class ↑ 𝑚
7 cr class ℝ
8 5 7 6 co class 0 +∞ ℝ
9 vx setvar x
10 vg setvar g
11 citg1 class ∫ 1
12 11 cdm class dom ⁡ ∫ 1
13 10 cv setvar g
14 cle class ≤
15 14 cofr class ∘ r ⁡ ≤
16 1 cv setvar f
17 13 16 15 wbr wff g ≤ f f
18 9 cv setvar x
19 13 11 cfv class ∫ 1 ⁡ g
20 18 19 wceq wff x = ∫ 1 ⁡ g
21 17 20 wa wff g ≤ f f ∧ x = ∫ 1 ⁡ g
22 21 10 12 wrex wff ∃ g ∈ dom ⁡ ∫ 1 g ≤ f f ∧ x = ∫ 1 ⁡ g
23 22 9 cab class x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f f ∧ x = ∫ 1 ⁡ g
24 cxr class ℝ *
25 clt class <
26 23 24 25 csup class sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f f ∧ x = ∫ 1 ⁡ g ℝ * <
27 1 8 26 cmpt class f ∈ 0 +∞ ℝ ⟼ sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f f ∧ x = ∫ 1 ⁡ g ℝ * <
28 0 27 wceq wff ∫ 2 = f ∈ 0 +∞ ℝ ⟼ sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f f ∧ x = ∫ 1 ⁡ g ℝ * <