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 24518
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 24513 . 2 class 2
2 vf . . 3 setvar 𝑓
3 cc0 10729 . . . . 5 class 0
4 cpnf 10864 . . . . 5 class +∞
5 cicc 12938 . . . . 5 class [,]
63, 4, 5co 7213 . . . 4 class (0[,]+∞)
7 cr 10728 . . . 4 class
8 cmap 8508 . . . 4 class m
96, 7, 8co 7213 . . 3 class ((0[,]+∞) ↑m ℝ)
10 vg . . . . . . . . 9 setvar 𝑔
1110cv 1542 . . . . . . . 8 class 𝑔
122cv 1542 . . . . . . . 8 class 𝑓
13 cle 10868 . . . . . . . . 9 class
1413cofr 7468 . . . . . . . 8 class r
1511, 12, 14wbr 5053 . . . . . . 7 wff 𝑔r𝑓
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1542 . . . . . . . 8 class 𝑥
18 citg1 24512 . . . . . . . . 9 class 1
1911, 18cfv 6380 . . . . . . . 8 class (∫1𝑔)
2017, 19wceq 1543 . . . . . . 7 wff 𝑥 = (∫1𝑔)
2115, 20wa 399 . . . . . 6 wff (𝑔r𝑓𝑥 = (∫1𝑔))
2218cdm 5551 . . . . . 6 class dom ∫1
2321, 10, 22wrex 3062 . . . . 5 wff 𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))
2423, 16cab 2714 . . . 4 class {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}
25 cxr 10866 . . . 4 class *
26 clt 10867 . . . 4 class <
2724, 25, 26csup 9056 . . 3 class sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < )
282, 9, 27cmpt 5135 . 2 class (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
291, 28wceq 1543 1 wff 2 = (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔r𝑓𝑥 = (∫1𝑔))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  itg2val  24626
  Copyright terms: Public domain W3C validator