Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-itgm Structured version   Unicode version

Definition df-itgm 26881
 Description: Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions. Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric sitm. He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 21237. (Contributed by Thierry Arnoux, 13-Feb-2018.)
Assertion
Ref Expression
df-itgm itgm measures metUnifsitmCnExtUnifStsitg
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-itgm
StepHypRef Expression
1 citgm 26858 . 2 itgm
2 vw . . 3
3 vm . . 3
4 cvv 3078 . . 3
5 cmeas 26755 . . . . 5 measures
65crn 4950 . . . 4 measures
76cuni 4200 . . 3 measures
82cv 1369 . . . . 5
93cv 1369 . . . . 5
10 csitg 26860 . . . . 5 sitg
118, 9, 10co 6201 . . . 4 sitg
12 csitm 26859 . . . . . . 7 sitm
138, 9, 12co 6201 . . . . . 6 sitm
14 cmetu 17934 . . . . . 6 metUnif
1513, 14cfv 5527 . . . . 5 metUnifsitm
16 cuss 19961 . . . . . 6 UnifSt
178, 16cfv 5527 . . . . 5 UnifSt
18 ccnext 19764 . . . . 5 CnExt
1915, 17, 18co 6201 . . . 4 metUnifsitmCnExtUnifSt
2011, 19cfv 5527 . . 3 metUnifsitmCnExtUnifStsitg
212, 3, 4, 7, 20cmpt2 6203 . 2 measures metUnifsitmCnExtUnifStsitg
221, 21wceq 1370 1 itgm measures metUnifsitmCnExtUnifStsitg
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator