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

Definition df-itg2 23196
 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 23191 . 2 class 2
2 vf . . 3 setvar 𝑓
3 cc0 9815 . . . . 5 class 0
4 cpnf 9950 . . . . 5 class +∞
5 cicc 12049 . . . . 5 class [,]
63, 4, 5co 6549 . . . 4 class (0[,]+∞)
7 cr 9814 . . . 4 class
8 cmap 7744 . . . 4 class 𝑚
96, 7, 8co 6549 . . 3 class ((0[,]+∞) ↑𝑚 ℝ)
10 vg . . . . . . . . 9 setvar 𝑔
1110cv 1474 . . . . . . . 8 class 𝑔
122cv 1474 . . . . . . . 8 class 𝑓
13 cle 9954 . . . . . . . . 9 class
1413cofr 6794 . . . . . . . 8 class 𝑟
1511, 12, 14wbr 4583 . . . . . . 7 wff 𝑔𝑟𝑓
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1474 . . . . . . . 8 class 𝑥
18 citg1 23190 . . . . . . . . 9 class 1
1911, 18cfv 5804 . . . . . . . 8 class (∫1𝑔)
2017, 19wceq 1475 . . . . . . 7 wff 𝑥 = (∫1𝑔)
2115, 20wa 383 . . . . . 6 wff (𝑔𝑟𝑓𝑥 = (∫1𝑔))
2218cdm 5038 . . . . . 6 class dom ∫1
2321, 10, 22wrex 2897 . . . . 5 wff 𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))
2423, 16cab 2596 . . . 4 class {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}
25 cxr 9952 . . . 4 class *
26 clt 9953 . . . 4 class <
2724, 25, 26csup 8229 . . 3 class sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < )
282, 9, 27cmpt 4643 . 2 class (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
291, 28wceq 1475 1 wff 2 = (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔𝑟𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  itg2val  23301
 Copyright terms: Public domain W3C validator