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

Definition df-itgm 30956
 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 23796. (Contributed by Thierry Arnoux, 13-Feb-2018.)
Assertion
Ref Expression
df-itgm itgm = (𝑤 ∈ V, 𝑚 ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
Distinct variable group:   𝑤,𝑚

Detailed syntax breakdown of Definition df-itgm
StepHypRef Expression
1 citgm 30930 . 2 class itgm
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3414 . . 3 class V
5 cmeas 30799 . . . . 5 class measures
65crn 5347 . . . 4 class ran measures
76cuni 4660 . . 3 class ran measures
82cv 1655 . . . . 5 class 𝑤
93cv 1655 . . . . 5 class 𝑚
10 csitg 30932 . . . . 5 class sitg
118, 9, 10co 6910 . . . 4 class (𝑤sitg𝑚)
12 csitm 30931 . . . . . . 7 class sitm
138, 9, 12co 6910 . . . . . 6 class (𝑤sitm𝑚)
14 cmetu 20104 . . . . . 6 class metUnif
1513, 14cfv 6127 . . . . 5 class (metUnif‘(𝑤sitm𝑚))
16 cuss 22434 . . . . . 6 class UnifSt
178, 16cfv 6127 . . . . 5 class (UnifSt‘𝑤)
18 ccnext 22240 . . . . 5 class CnExt
1915, 17, 18co 6910 . . . 4 class ((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))
2011, 19cfv 6127 . . 3 class (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚))
212, 3, 4, 7, 20cmpt2 6912 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
221, 21wceq 1656 1 wff itgm = (𝑤 ∈ V, 𝑚 ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator