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

Definition df-itg2 24263
 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 24258 . 2 class 2
2 vf . . 3 setvar 𝑓
3 cc0 10541 . . . . 5 class 0
4 cpnf 10676 . . . . 5 class +∞
5 cicc 12746 . . . . 5 class [,]
63, 4, 5co 7142 . . . 4 class (0[,]+∞)
7 cr 10540 . . . 4 class
8 cmap 8404 . . . 4 class m
96, 7, 8co 7142 . . 3 class ((0[,]+∞) ↑m ℝ)
10 vg . . . . . . . . 9 setvar 𝑔
1110cv 1537 . . . . . . . 8 class 𝑔
122cv 1537 . . . . . . . 8 class 𝑓
13 cle 10680 . . . . . . . . 9 class
1413cofr 7396 . . . . . . . 8 class r
1511, 12, 14wbr 5033 . . . . . . 7 wff 𝑔r𝑓
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1537 . . . . . . . 8 class 𝑥
18 citg1 24257 . . . . . . . . 9 class 1
1911, 18cfv 6329 . . . . . . . 8 class (∫1𝑔)
2017, 19wceq 1538 . . . . . . 7 wff 𝑥 = (∫1𝑔)
2115, 20wa 399 . . . . . 6 wff (𝑔r𝑓𝑥 = (∫1𝑔))
2218cdm 5522 . . . . . 6 class dom ∫1
2321, 10, 22wrex 3107 . . . . 5 wff 𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))
2423, 16cab 2776 . . . 4 class {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}
25 cxr 10678 . . . 4 class *
26 clt 10679 . . . 4 class <
2724, 25, 26csup 8903 . . 3 class sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < )
282, 9, 27cmpt 5113 . 2 class (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
291, 28wceq 1538 1 wff 2 = (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  itg2val  24370
 Copyright terms: Public domain W3C validator