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

Definition df-itg2 24151
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 2 = (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
Distinct variable group:   𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-itg2
StepHypRef Expression
1 citg2 24146 . 2 class 2
2 vf . . 3 setvar 𝑓
3 cc0 10526 . . . . 5 class 0
4 cpnf 10661 . . . . 5 class +∞
5 cicc 12731 . . . . 5 class [,]
63, 4, 5co 7145 . . . 4 class (0[,]+∞)
7 cr 10525 . . . 4 class
8 cmap 8396 . . . 4 class m
96, 7, 8co 7145 . . 3 class ((0[,]+∞) ↑m ℝ)
10 vg . . . . . . . . 9 setvar 𝑔
1110cv 1527 . . . . . . . 8 class 𝑔
122cv 1527 . . . . . . . 8 class 𝑓
13 cle 10665 . . . . . . . . 9 class
1413cofr 7397 . . . . . . . 8 class r
1511, 12, 14wbr 5058 . . . . . . 7 wff 𝑔r𝑓
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1527 . . . . . . . 8 class 𝑥
18 citg1 24145 . . . . . . . . 9 class 1
1911, 18cfv 6349 . . . . . . . 8 class (∫1𝑔)
2017, 19wceq 1528 . . . . . . 7 wff 𝑥 = (∫1𝑔)
2115, 20wa 396 . . . . . 6 wff (𝑔r𝑓𝑥 = (∫1𝑔))
2218cdm 5549 . . . . . 6 class dom ∫1
2321, 10, 22wrex 3139 . . . . 5 wff 𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))
2423, 16cab 2799 . . . 4 class {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}
25 cxr 10663 . . . 4 class *
26 clt 10664 . . . 4 class <
2724, 25, 26csup 8893 . . 3 class sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < )
282, 9, 27cmpt 5138 . 2 class (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
291, 28wceq 1528 1 wff 2 = (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  itg2val  24258
  Copyright terms: Public domain W3C validator