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 23313
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[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
Distinct variable group:   𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-itg2
StepHypRef Expression
1 citg2 23308 . 2 class 2
2 vf . . 3 setvar 𝑓
3 cc0 9888 . . . . 5 class 0
4 cpnf 10023 . . . . 5 class +∞
5 cicc 12128 . . . . 5 class [,]
63, 4, 5co 6610 . . . 4 class (0[,]+∞)
7 cr 9887 . . . 4 class
8 cmap 7809 . . . 4 class 𝑚
96, 7, 8co 6610 . . 3 class ((0[,]+∞) ↑𝑚 ℝ)
10 vg . . . . . . . . 9 setvar 𝑔
1110cv 1479 . . . . . . . 8 class 𝑔
122cv 1479 . . . . . . . 8 class 𝑓
13 cle 10027 . . . . . . . . 9 class
1413cofr 6856 . . . . . . . 8 class 𝑟
1511, 12, 14wbr 4618 . . . . . . 7 wff 𝑔𝑟𝑓
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1479 . . . . . . . 8 class 𝑥
18 citg1 23307 . . . . . . . . 9 class 1
1911, 18cfv 5852 . . . . . . . 8 class (∫1𝑔)
2017, 19wceq 1480 . . . . . . 7 wff 𝑥 = (∫1𝑔)
2115, 20wa 384 . . . . . 6 wff (𝑔𝑟𝑓𝑥 = (∫1𝑔))
2218cdm 5079 . . . . . 6 class dom ∫1
2321, 10, 22wrex 2908 . . . . 5 wff 𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))
2423, 16cab 2607 . . . 4 class {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}
25 cxr 10025 . . . 4 class *
26 clt 10026 . . . 4 class <
2724, 25, 26csup 8298 . . 3 class sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < )
282, 9, 27cmpt 4678 . 2 class (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
291, 28wceq 1480 1 wff 2 = (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  itg2val  23418
  Copyright terms: Public domain W3C validator